1\DOC export_rewrites
2
3\TYPE {export_rewrites : string list -> unit}
4
5\SYNOPSIS
6Exports theorems so that they merge with the ``stateful'' rewriter's {simpset}.
7
8\KEYWORDS
9simplification
10
11\DESCRIBE
12A call to {export_rewrites strlist} causes the theorems named by the
13strings in {strlist} to be merged into the {simpset} value maintained
14behind the function {srw_ss()}, both in the current session and also
15when the theory generated by the script file is loaded.
16
17Theorems are named by giving the name of the segment, a full-stop (or
18period) character, and the name of theorem. If the theorem is in the
19current segment, the segment can be omitted. Thus, if working in the
20development of the theory of lists, the following are valid names
21{list.MAP_GENLIST}, {MAP_GENLIST} and {arithmetic.LESS_TRANS}.
22
23The collection of all the theorems specified in calls to
24{export_rewrites} can be obtained as a value of type {simpLib.ssfrag}
25using the {thy_ssfrag} function.
26
27Multiple calls to {export_rewrites} cumulatively add to the list of
28theorems being exported.
29
30\FAILURE
31Fails if any of the strings in the list does not name a theorem in the
32current context.
33
34\COMMENTS
35This function is useful for ensuring that the stateful rewriter is
36augmented as theories are loaded.  This in turn means that users of
37these theories don't need to learn the names of their ``obvious''
38theorems.  Because theorems can not be removed from the stateful
39rewriter's underlying {simpset}, choice of ``obvious'' theorems needs
40to be done with care.
41
42\SEEALSO
43bossLib.augment_srw_ss, bossLib.srw_ss, bossLib.SRW_TAC, BasicProvers.thy_ssfrag.
44
45\ENDDOC
46