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

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



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