next up previous contents
Next: Proof Environment Management Up: The Desktop Environment Previous: The Desktop Environment

Loading and Saving Theories

Theory files are saved with a fixed extension (currently .wthy). They are script files written using commands of the alternative interface invoked by the walk command which reconstruct all information in the theory.

There is an environment variable representing the name of the current theory, which can be read using the theoryname command. The storeall command sets the theory name to its parameter and stores the theory in a file with name obtained by adding the extension to the theory name. The safesave command saves a theory to the file whose name is indicated by the current theory name variable. The load command sets the theory name environment variable to its parameter and loads the appropriate theory file (automatically backing up the current theory on the desktop).

The clear command will clear the current theory; the cleartheories command will clear all theories from the desktop.

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