Next: Definition Commands
Up: Appendix: Reference for Individual
Previous: Proof 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
- ``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''
- ``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'').
Fri Sep 5 16:28:58 MDT 1997