export_rewrites
BasicProvers.export_rewrites : string list -> unit
Exports theorems so that they merge with the "stateful" rewriter's
simpset.
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.
See also
bossLib.augment_srw_ss,
bossLib.srw_ss,
bossLib.SRW_TAC,
BasicProvers.thy_ssfrag