SIMP_RULE

simpLib.SIMP_RULE : simpset -> thm list -> thm -> thm

Simplify a term with the given simpset and theorems.

bossLib.SIMP_RULE is identical to simpLib.SIMP_RULE.

See also

bossLib.SIMP_RULE