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.

Fri Sep 5 16:28:58 MDT 1997