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.