----------------------------------------------------------------------
save_thm                                                      (Theory)
----------------------------------------------------------------------
save_thm : string * thm -> thm

SYNOPSIS
Stores a theorem in the current theory segment.

DESCRIBE
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
Theory.new_theory, Tactical.store_thm, DB.fetch, DB.thy,
Theory.current_definitions, Theory.current_theorems,
Theory.uptodate_thm, Theory.new_axiom, Definition.new_type_definition,
Definition.new_definition, Definition.new_specification.

----------------------------------------------------------------------