SIMP_TAC

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

Simplify a term with the given simpset and theorems.

bossLib.SIMP_TAC is identical to simpLib.SIMP_TAC.

See also

bossLib.SIMP_TAC