REV_FULL_SIMP_TAC

bossLib.REV_FULL_SIMP_TAC : simpset -> thm list -> tactic

Simplifies the goal (assumptions as well as conclusion) with the given simpset.

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.

See also

bossLib.FULL_SIMP_TAC, bossLib.ASM_SIMP_TAC, bossLib.SIMP_TAC