**applythm**- ``applythm thm'' applies the theorem ``thm'', but
without executing any embedded theorems introduced. ``thm'' may be
supplied with parameters.
**applyconvthm**- As ``applythm'', but in the reverse direction.
**applyenv, applyconvenv**- As the previous two commands, but using
saved environments.
**reprove**- ``reprove thm'' allows the current equation to be
stored as ``thm'', where ``thm'' already exists, with the sole
constraint being that the new version of ``thm'' must depend on no
more axioms than the old version of ``thm''.
**autoreprove**- Same effect as ``reprove'', with the same
restriction, with the argument set to the ``current theorem''
environment variable.
**getleftside**- ``getleftside thm'' gets left side of theorem as
both sides of current equation and sets ``current theorem'' to
``thm''. Saves old environment on desktop. (walk command ``L'').
**getrightside**- As ``getleftside'', but the right side of the
theorem. (walk command ``R'').
**autoedit**- ``autoedit theorem'' sets the current equation to
``theorem'', and sets the current theorem environment variable to
``theorem'' (with parameters, if any). (saves old environment on
desktop). (walk command ``E'').

Fri Sep 5 16:28:58 MDT 1997