Next: Proof Environment and Theorem
Up: Command Reference
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
- 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
- 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
- Save the current proof environment under its own
name or as ``backup'' if its name is the default.
Fri Sep 5 16:28:58 MDT 1997