bossLib.augment_srw_ss : simpLib.ssfrag list -> unit
STRUCTURE
SYNOPSIS
Augments the “stateful rewriter” with a list of simpset fragments.
LIBRARY
bossLib
DESCRIPTION
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.
SEEALSO
HOL  Kananaskis-10