Proof commands:

defineconstant:

This command takes two arguments, both terms. If the equation of the first term to the second has the correct form, the atomic constant ``head'' of the first term is defined (if undeclared) using the equation, which is postulated as a theorem with the same name.

definetypedinfix:

This command takes five arguments, a string followed by two integers, followed by two strings. The first string is intended to be a (so far undeclared) theorem name. The integer arguments are the left and right types of the operator to be defined. If the equation of the last two arguments has the correct form (and is stratified), the operator ``head'' (if undeclared) is defined using that equation: the first argument is the name of the new theorem.

defineinfix:

This command takes three arguments, all strings. It has the same effect as definetypedinfix with second and third arguments of 0 inserted between the first string argument and the other two: this command defines ``flat'' infixes.

typedefinition:

Now superseded by the commands below.

defineconstanttype:

Takes three term arguments. The second is a type expression using a constant type or function type constructor; the third is an expression defining the type expression. The first argument is the name of a theorem proving that the defined operation is a retraction.

defineinfixtype:

Takes four arguments. The third is a type expression using an operator type constructor; the fourth is an expression defining the type expression. The second argument is the name of a theorem proving that the defined operation is a retraction. The first argument is the name of the new definition theorem. The new type constructor is an opaque operator.

axiom:

The axiom command takes three string arguments. The first argument is the name of the axiom to be introduced, the second is its left side, and the third is its right side. a is an abbreviation for axiom.

statement:

The statement command takes two string arguments. The first argument is the name of an axiom to be introduced; the second is its left side, while the right side will be true.

proveanaxiom:

This command takes one string argument, the name of an axiom. If the equation under construction is identical to the axiom to be proved, and does not have axiomatic dependencies on the axiom to be proved, the erstwhile axiom is assigned the dependencies of the current environment and the dependencies of all theorems are changed to reflect this.

makeanaxiom:

This command takes one string argument, the name of a theorem. This theorem is made an axiom.

undefine:

This command takes one string argument, a constant or operator. The definition of this constant or operator is converted to an axiom.

makeadefinition:

This command takes one string argument, the name of an axiom. If this axiom has the correct form, it is converted to a definition (this will not happen if there is a conflict with an existing definition). Type definitions not supported.

prove:

This command takes one string argument, a term. The term needs to be of the correct form so that its constant or operator ``head'' (which must be undeclared) can be declared as a theorem with left and right side taken from the equation under construction. The term argument supplies not only the name of the theorem but also the form of parameter list it takes (if any). p is an abbreviation for prove.

reprove:

This command takes one string argument, a term. The command works just as prove, except that the name of the theorem to be proved must already be in use (it will be replaced). The restrictions on adding new dependencies found in Mark2 no longer hold. rp is an abbreviation for reprove.

autoreprove:

This command takes a unit argument. It has the same effect as reprove, except that the ``format'' of the current environment (a feature set only by the autoedit, getleftside, and getrightside commands) is supplied as the argument of reprove. Usually used in conjunction with autoedit or its relations.

verify:

This command takes a string argument. If the currently displayed term matches the argument, it does nothing; otherwise it issues an error message.

clearerrorflag:

This command takes a unit argument. It clears the error flag which is raised when error messages are issued and prevents proofs from being carried out. cef is an abbreviation for this command.

forget:

This command takes a single string argument, the name of a theorem. That theorem and all theorems which refer to it are ``forgotten''. Axioms and definitions cannot be forgotten (one can do this with work by using the reaxiomatization and redefinition commands). forget has not yet been harmonized with the new incremental backup scheme.