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