rewrites : thm list -> ssfrag
STRUCTURE
simpLib
SYNOPSIS
Create an
ssfrag
value consisting of the given theorems as rewrites.
DESCRIBE
bossLib.rewrites
is identical to
simpLib.rewrites
.
SEEALSO
rewrites
HOL
Kananaskis-4