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.