REV_FULL_SIMP_TAC : simpset -> thm list -> tactic
STRUCTURE
SYNOPSIS
Simplifies the goal (assumptions as well as conclusion) with the given simpset.
LIBRARY
simpLib
DESCRIPTION
REV_FULL_SIMP_TAC is the same as FULL_SIMP_TAC except that it simplifies the assumptions in the opposite order.

That is, in REV_FULL_SIMP_TAC, each assumption is used to rewrite higher-numbered assumptions, whereas in FULL_SIMP_TAC, each assumption is used to rewrite lower-numbered assumptions.

SEEALSO
HOL  Kananaskis-13