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