rewrites

simpLib.rewrites : thm list -> ssfrag

Create an ssfrag value consisting of the given theorems as rewrites.

bossLib.rewrites is identical to simpLib.rewrites.

See also

bossLib.rewrites