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

Tactic Language Interpreter

The trace/debug command for the tactic language; executes one step in current subterm each time a key is pressed. Hit ``q'' to break out; terminates automatically if the term stabilizes.

More limited trace/debug command; executes just one step in current subterm.

The tactic language interpreter; executes all embedded theorems or tactics in the current subterm, and all embedded theorems or tactics newly invoked in this way, using an aggressive depth-first strategy. (walk command ``e'').

Warning (for all these commands):
If you break out of any tactic interpreter using Control-C, use the ``top'' command to reset environment variables.

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