**ruleintro**- ``ruleintro theorem'' introduces an embedded
occurrence of ``theorem'' at the current subterm. (walk command ``i'').
**revruleintro**- As ``ruleintro'', except that the theorem is to
be applied in the reverse direction, (walk command ``v'').
**undelay**- Remove a ``delay'' prefix from the current subterm.
**delay**- Introduce a ``delay'' prefix to the current subterm.
**unlazy, lazy**- As ``undelay'' or ``delay'' with the full
laziness prefix.
**altrule**- Converts an embedded theorem at the current subterm between the normal and alternative forms. (walk command ``f'').
**droprule**- Drops an embedded theorem from top of current subterm
(if there is one).
**proveprogram**- ``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
functional programming.
**deprogram**- ``deprogram name'' removes the theorem bound to
``name''.

Fri Sep 5 16:28:58 MDT 1997