Next: Assignment Commands
Up: Appendix: Reference for Individual
Previous: Definition Commands
- ``ruleintro theorem'' introduces an embedded
occurrence of ``theorem'' at the current subterm. (walk command ``i'').
- As ``ruleintro'', except that the theorem is to
be applied in the reverse direction, (walk command ``v'').
- Remove a ``delay'' prefix from the current subterm.
- Introduce a ``delay'' prefix to the current subterm.
- unlazy, lazy
- As ``undelay'' or ``delay'' with the full
- Converts an embedded theorem at the current subterm
between the normal and alternative forms. (walk command ``f'').
- Drops an embedded theorem from top of current subterm
(if there is one).
- ``proveprogram name thm'' causes the theorem
``thm'' to be applied wherever the constant or operator ``name''
appears in a context defined by the left side of ``thm''. Simulates
- ``deprogram name'' removes the theorem bound to
Fri Sep 5 16:28:58 MDT 1997