Rule Introduction Commands

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