----------------------------------------------------------------------
export_rewrites                                         (BasicProvers)
----------------------------------------------------------------------
export_rewrites : string list -> unit

SYNOPSIS
Exports theorems so that they merge with the “stateful” rewriter’s {simpset}.

KEYWORDS
simplification

DESCRIBE
A call to {export_rewrites strlist} causes the theorems named by the
strings in {strlist} to be merged into the {simpset} value maintained
behind the function {srw_ss()}, both in the current session and also
when the theory generated by the script file is loaded.

Theorems are named by giving the name of the segment, a full-stop (or
period) character, and the name of theorem. If the theorem is in the
current segment, the segment can be omitted. Thus, if working in the
development of the theory of lists, the following are valid names
{list.MAP_GENLIST}, {MAP_GENLIST} and {arithmetic.LESS_TRANS}.

The collection of all the theorems specified in calls to
{export_rewrites} can be obtained as a value of type {simpLib.ssfrag}
using the {thy_ssfrag} function.

Multiple calls to {export_rewrites} cumulatively add to the list of
theorems being exported.

FAILURE
Fails if any of the strings in the list does not name a theorem in the
current context.

COMMENTS
This function is useful for ensuring that the stateful rewriter is
augmented as theories are loaded.  This in turn means that users of
these theories don’t need to learn the names of their “obvious”
theorems.  Because theorems can not be removed from the stateful
rewriter’s underlying {simpset}, choice of “obvious” theorems needs
to be done with care.

SEEALSO
bossLib.augment_srw_ss, bossLib.srw_ss, bossLib.SRW_TAC,
BasicProvers.thy_ssfrag.

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