next up previous contents
Next: The Module System Up: The Proof Environment Previous: Global Variable Assignment

Finishing Up

The basic command for completing a session is prove, which takes as a parameter the format of the theorem to be proved (the name plus any parameters).

If the name/format environment variable has been set (this can be ascertained using the envname command), the command autoprove will record the current equation as a theorem with the format indicated by the environment variable.

The reprove command allows one to modify an existing theorem, replacing it with the current equation. Normally, this is used for debugging tactics. The only constraint is that the new version of the theorem cannot have stronger dependencies than the old; if this were not enforced, the dependency information of tactics which invoke the edited theorem would be corrupted.

The autoreprove variant of this command is often used, because the getleftside, getrightside, and autoedit commands, which are often used for editing, all set the name/format environment variable.

A proof environment does not close down when a theorem is proved; the current equation remains the same until a new command in the start family is issued. In this case, the current equation is usually automatically backed up (the backupenv command is invoked).

When a new theorem environment is started up, the attempt to back up the previous theorem environment will generate an error message applying to that previous environment if there is something wrong with it.

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