Theory.export

STRUCTURE

SYNOPSIS

Write a theory segment to disk.

DESCRIPTION

An invocation export_theory() saves the current theory segment to disk. All parents, definitions, axioms, and stored theorems of the segment are saved in such a way that, when the theory is loaded from disk in a later session, the full theory in place at the time export_theory was called is re-instated.

If the current theory segment is named thy, then export_theory() will create ML files thyTheory.sig and thyTheory.sml, in the current directory at the time export_theory is invoked. These files need to be compiled before they become usable. In the standard way of doing things, the Holmake facility will handle this task.

Once a theory segment has been exported and compiled, it is available for use. It can be brought into an interactive proof session via

   load "thyTheory";

When the segment is loaded, its parents, axioms, theorems, and definitions are incorporated into the current theory (recall that this notion is different than the current theory segment).

FAILURE

A call to export_theory may fail if the disk file cannot be opened. A call to export_theory will also fail if some bindings are such that the name of the binding is not a valid ML identifier. In that case, export_theory will report all such bad names. These can be changed with set_MLname, and then export_theory may be attempted again.

EXAMPLE

- save_thm("foo", REFL (Term `x:bool`));
> val it = |- x = x : thm

- export_theory();
Exporting theory "scratch" ... done.
> val it = () : unit

COMMENTS

Note that export_theory exports the state of the theory, and not that of the ML environment. If one wants to restore the state of the ML environment in existence at the time export_theory() is invoked, special steps have to be taken; see adjoin_to_theory.

SEEALSO

new_theory, adjoin_to_theory, set_MLname