1\DOC export_theory 2 3\TYPE {export_theory : unit -> unit} 4 5\SYNOPSIS 6Write a theory segment to disk. 7 8\KEYWORDS 9theory, export, file. 10 11\DESCRIBE 12An invocation {export_theory()} saves the current theory segment to disk. 13All parents, definitions, axioms, and stored theorems of the segment 14are saved in such a way that, when the theory is loaded from disk 15in a later session, the full theory in place at the time 16{export_theory} was called is re-instated. 17 18If the current theory segment is named {thy}, then {export_theory()} 19will create ML files {thyTheory.sig} and {thyTheory.sml}, in 20the current directory at the time {export_theory} is invoked. These 21files need to be compiled before they become usable. In the standard way 22of doing things, the {Holmake} facility will handle this task. 23 24Once a theory segment has been exported and compiled, it is available 25for use. It can be brought into an interactive proof session via 26{ 27 load "thyTheory"; 28} 29 30When the segment is loaded, its parents, axioms, theorems, and 31definitions are incorporated into the current theory (recall that this 32notion is different than the current theory segment). 33 34\FAILURE 35A call to {export_theory} may fail if the disk file cannot be opened. 36A call to {export_theory} will also fail if some bindings are such that 37the name of the binding is not a valid ML identifier. In that case, 38{export_theory} will report all such bad names. These can be changed with 39{set_MLname}, and then {export_theory} may be attempted again. 40 41\EXAMPLE 42{ 43- save_thm("foo", REFL (Term `x:bool`)); 44> val it = |- x = x : thm 45 46- export_theory(); 47Exporting theory "scratch" ... done. 48> val it = () : unit 49} 50 51 52\COMMENTS 53Note that {export_theory} exports the state of the 54theory, and not that of the ML environment. If one wants to restore 55the state of the ML environment in existence at the time 56{export_theory()} is invoked, special steps have to be taken; 57see {adjoin_to_theory}. 58 59\SEEALSO 60Theory.new_theory, Theory.adjoin_to_theory, Theory.set_MLname. 61 62\ENDDOC 63