**axiom**- ``axiom name left-side right-side'' causes an axiom with
name ``name'', left side ``left-side'' and right side ``right-side''
to be created.
**interaxiom**- If the current subterm is an equation, ``interaxiom
axiom'' introduces it as an axiom called ``axiom''. (walk command ``x'').
**makeanaxiom**- ``makeanaxiom thm'' makes theorem ``thm'' an axiom.
**proveanaxiom**- If the current equation proves an axiom ``axiom''
(verbatim) from other axioms, the command ``proveanaxiom axiom''
will reset dependencies globally to reflect this fact.
**prove**- ``prove thm'' stores the current equation as ``thm''.
``thm'' may have variable parameters. (walk command ``p'').
**autoprove**- Stores the current equation as a theorem with name
the ``current theorem'' environment variable.
**reprove**- See editing commands
**autoreprove**- See editing commands
**redefinition commands**- See the newer Command Reference.
**module system commands**- See the newer Command Reference.

Fri Sep 5 16:28:58 MDT 1997