FULL_SIMP_TAC

simpLib.FULL_SIMP_TAC : simpset -> thm list -> tactic

Simplify a term with the given simpset and theorems.

bossLib.FULL_SIMP_TAC is identical to simpLib.FULL_SIMP_TAC.

See also

bossLib.FULL_SIMP_TAC