Next: Theory Desktop Commands
Up: Appendix: Reference for Individual
Previous: Assignment Commands
- 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
Fri Sep 5 16:28:58 MDT 1997