Editing Commands

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'').