rewrites
bossLib.rewrites : thm list -> ssfrag
Also exported as simpLib.rewrites.
Creates an ssfrag value consisting of the given theorems as rewrites.
Failure
Never fails.
Example
Instead of writing the simpler SIMP_CONV std_ss thmlist, one could
write
SIMP_CONV (std_ss ++ rewrites thmlist) []
More plausibly, rewrites can be used to create commonly used ssfrag
values containing a great number of rewrites. This is how the basic
system's various ssfrag values are constructed where those values
consist only of rewrite theorems.
See also
bossLib.++,
simpLib.mk_simpset,
simpLib.SSFRAG,
bossLib.SIMP_CONV