SIMP_RULE : simpset -> thm list -> thm -> thm
STRUCTURE
simpLib
SYNOPSIS
Simplify a term with the given simpset and theorems.
DESCRIPTION
bossLib.SIMP_RULE
is identical to
simpLib.SIMP_RULE
.
SEEALSO
SIMP_RULE
HOL
Trindemossen-1