Features of the Proof Environment

The proof environment is a data structure containing the following elements:

name:

The environment has a name. This may take the form of a term serving as the default format for the theorem to be proved (name and parameters). It is not necessary for the user to set the name. It is automatically set by certain commands, and it can be viewed using the envname command.

left side of theorem:

This is often but not always the term originally entered by the user. Assignment commands affect both sides of the current equation, and it is possible to switch the two sides using the workback command.

right side of theorem:

This is the term being viewed by the user.

position of selected subterm:

A list of booleans is used to indicate the selected subterm; an integer representing the number of nested variable binding contexts in which it is found is also provided.

current dependencies:

Axioms and definitions on which the proof so far depends are listed. Such information is maintained as an element of theorems and tactics as well.

The data structure representing a stored theorem has exactly the same structure, except that it does not include a ``position of selected subterm'', and it includes an additional component supporting the module system described below. The system takes advantage of this; saved proof environments are kept on the theorem list, though they cannot be used as theorems.