----------------------------------------------------------------------
srw_ss                                                       (bossLib)
----------------------------------------------------------------------
srw_ss : unit -> simpset

SYNOPSIS
Returns the "stateful rewriting" system’s underlying {simpset}.

KEYWORDS
simplification

LIBRARY
bossLib

DESCRIBE
A call to {srw_ss()} returns a {simpset} value that is internally
maintained and updated by the system.  Its value changes as new types
enter the {TypeBase}, and as theories are loaded.  For this reason, it
can’t be accessed as a simple value, but is instead hidden behind a
function.

The value behind {srw_ss()} can change in three ways.  Firstly, 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.

FAILURE
Never fails.

SEEALSO
bossLib.augment_srw_ss, BasicProvers.export_rewrites, bossLib.SRW_TAC.

----------------------------------------------------------------------