next up previous contents
Next: Theory Management Up: The Desktop Environment Previous: Loading and Saving Theories

Proof Environment Management

Proof environments can be saved on the desktop while working in a particular theory. When a theory is saved on the desktop, all associated environments are saved with it (this is also true when theories are saved to files, since environments are stored on the theorem list).

The saveenv command allows one to save a proof environment, specifying a name/format to be associated with that environment. The backupenv command sets the name/format of the saved environment to the current name/format environment variable if set by the user or to backup. The getenv environment loads a saved environment; it will issue a warning if this environment was found only on the theorem list and not on the current desktop. The getenv command and most commands of the start family automatically invoke backupenv. An exception is if one is actually using getenv to retrieve the backup of the current environment!

dropenv will delete an environment (from the theorem list and the desktop) and clearenvs will eliminate all saved environments. loadsavedenvs allows one to load all saved environments in a theory file onto the desktop (one must hit return to load each such environment as in the thmdisplay family of commands); this can be useful if one wants to clear all such environments without loading them onto the desktop individually.



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