The basic command for starting out is the `start` command, which
takes the initial version of the left side of the equation as a
parameter. A variant is the `startfor` command, which has two
parameters, the name or format of the theorem to be proved and the
initial term.

The `getleftside` and `getrightside` commands allow one to get
one side of a theorem as the initial term in a new proof session, in
which the name/format environment variable will automatically be set
to the theorem name or format. The `autoedit` command creates a
proof session identical to that one has obtained when one proves the
theorem, and sets the name/format to the name or format of the
theorem.

The `getenv` command allows one to get a proof environment saved
by name; `saveenv` or `backupenv` (the former takes a
name/format as a parameter; the latter uses the current name/format or
a default) allow one to save proof environments on the desktop.

Fri Sep 5 16:28:58 MDT 1997