SIMP_CONV

simpLib.SIMP_CONV : simpset -> thm list -> conv

Simplify a term with the given simpset and theorems.

bossLib.SIMP_CONV is identical to simpLib.SIMP_CONV.

See also

bossLib.SIMP_CONV