next up previous contents
Next: Proof Environment and Theorem Up: Command Reference Previous: Desktop


A workspace consists of a number of ``saved'' proof environments, all associated with the same theory, whose name is the name of the workspace, and a current proof environment (one of the ``saved'' environments may be an older version of the current one).

Workspace commands include

See the name of the current theory.

start <term>:
Create a proof environment, with name a default, and with the term under consideration given by the argument. Any existing proof environment is backed up.

startfor <term> <term>:
As ``start'', except that the name of the proof environment is specified by the first term argument.

getleftside or getrightside <string>:
Create a new proof environment with starting term the appropriate side of the theorem indicated by the argument and name set to the ``format'' of that theorem.

autoedit <string>:
Creates a proof environment with name, left side of equation and right side of equation determined by the theorem whose name is the argument.

getenv <term>:
Get the proof environment named by the argument, backing up the current one unless the current one is the one being retrieved.

saveenv <term>:
Save the current proof environment with the indicated name.

Save the current proof environment under its own name or as ``backup'' if its name is the default.

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