Workspace

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

theoryname

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.

backupenv:

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