next up previous contents
Next: Editing Commands Up: Appendix: Reference for Individual Previous: Theorem Display Commands

Proof Commands

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.



Randall Holmes
Fri Sep 5 16:28:58 MDT 1997