next up previous contents
Next: Definition Commands Up: Appendix: Reference for Individual Previous: Proof Commands

Editing Commands

``applythm thm'' applies the theorem ``thm'', but without executing any embedded theorems introduced. ``thm'' may be supplied with parameters.

As ``applythm'', but in the reverse direction.

applyenv, applyconvenv
As the previous two commands, but using saved environments.

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

Same effect as ``reprove'', with the same restriction, with the argument set to the ``current theorem'' environment variable.

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

As ``getleftside'', but the right side of the theorem. (walk command ``R'').

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

Randall Holmes
Fri Sep 5 16:28:58 MDT 1997