augment_srw_ss
bossLib.augment_srw_ss : simpLib.ssfrag list -> unit
Also exported as BasicProvers.augment_srw_ss.
Augments the "stateful rewriter" with a list of simpset fragments.
A call to augment_srw_ss sslist causes each element of sslist to be
merged into the simpset value that the system maintains "behind"
srw_ss().
Failure
Never fails.
Comments
The change to the srw_ss() simpset brought about with
augment_srw_ss is not exported with a theory, so it is not
"permanent". But see export_rewrites for a simple way to achieve a
sort of permanence.
See also
BasicProvers.export_rewrites,
bossLib.srw_ss,
bossLib.SRW_TAC