next up previous contents
Next: Declaring Pretheorems Up: The Proof Environment Previous: The Proof Environment

Proving Theorems

When the current equation is in the desired form, the command prove is issued. The argument of this command will either be a name for the theorem, in which case the theorem is simply recorded with that name, or, in the case of a parameterized theorem, it may be a ``format'' for the theorem, which can take exactly the same forms as the left side of a definition. In either event, the name of the theorem (which may in the latter case be an operator) cannot have been declared already and will automatically be declared as a constant or operator. Variants on the prove command are discussed in a later section.

Note that the definition facility provides another way to prove theorems of a special form. The axiom and interaxiom commands allow one to introduce axioms.

The forget command eliminates a theorem and all theorems which refer to it or depend on it. It is extremely slow, and it is not especially reliable.





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