The value behind srw_ss() can change in three ways. First, whenever a type enters the TypeBase, the type’s associated simplification theorems (accessible directly using the function TypeBase.simpls_of) are all added to the simpset. This ensures that the "obvious" rewrite theorems for a type (such as the disjointness of constructors) need never be explicitly specified.

Secondly, users can interactively add simpset fragments to the srw_ss() value by using the function augment_srw_ss. This function might be used after a definition is made to ensure that a particular constant always has its definition expanded. (Whether or not a constant warrants this is something that needs to be determined on a case-by-case basis.)

Thirdly, theories can augment the srw_ss() value as they load. This is set up in a theory’s script file with the function export_rewrites. This causes a list of appropriate theorems to be added when the theory loads. It is up to the author of the theory to ensure that the theorems added to the simpset are sensible.