save_thm : string * thm -> thm
STRUCTURE
Theory
SYNOPSIS
Stores a theorem in the current theory segment.
DESCRIPTION
The call save_thm(name, th) adds the theorem th to the current theory segment under the name name. The theorem is also the return value of the call. When the current segment thy is exported, things are arranged in such a way that, if thyTheory is loaded into a later session, the ML variable thyTheory.name will have th as its value.
FAILURE
If th is out-of-date, then save_thm will fail. If name is not a valid ML alphanumeric identifier, save_thm will not fail, but export_theory will (printing an informative error message first).
EXAMPLE
- val foo = save_thm("foo", REFL (Term `x:bool`));
> val foo = |- x = x : thm

- current_theorems();
> val it = [("foo", |- x = x)] : (string * thm) list

COMMENTS
If a theorem is already saved under name in the current theory segment, it will be overwritten.

The results of new_axiom, and definition principle (such as new_definition, new_type_definition, and new_specification) are automatically stored in the current theory: one does not have to call save_thm on them.

USES
Saving important theorems for eventual export. Binding the result of save_thm to an ML variable makes it easy to access the theorem in the remainder of the current session.
SEEALSO
new_theory, store_thm, fetch, thy, current_definitions, current_theorems, uptodate_thm, new_axiom, new_type_definition, new_definition, new_specification
HOL  Kananaskis-14