Theorems are stored with dependency information, a list of the names of axioms and definitions on which they depend. The dependency structure of a theory can be completely restructured.

The `makeanaxiom` command can force a theorem to become an axiom;
the `proveanaxiom` command allows one to eliminate an axiom by
exhibiting a proof of it from other axioms, with appropriate global
dependency modifications. These tools can be used to support the use
of lemmas before they are proved.

The `defineprimitive` command will convert a theorem into a
definition of a primitive constant or operator if it has the right
form. The `redefineconstant` or `redefineinfix` command will
replace one definition of a constant or operator (resp.) by another,
with appropriate dependency modifications. The `undefine`
operator converts a definition to an axiom.

The elimination of unneeded dependencies on definitions (due to the
defined object not being mentioned) should be handled automatically by
the proof commands; this is the operational difference between a
definition and an axiom. At the moment, however, performance problems
with the function which removes unwanted dependencies on definitions
make it necessary to remove all automatic applications; the user may
apply the temporary `reallyremovedefdeps` command to effect such
reductions of dependencies manually.

Fri Sep 5 16:28:58 MDT 1997