**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.