ACL2-PC::COMMANDS

(macro) display instructions from the current interactive session
Major Section:  PROOF-CHECKER-COMMANDS

Examples:
commands
(commands 10 t)

General Forms:

commands or (commands nil) Print out all the instructions (in the current state-stack) in reverse order, i.e. from the most recent instruction to the starting instruction.

(commands n) [n a positive integer] Print out the most recent n instructions (in the current state-stack), in reverse order.

(commands x abbreviate-flag) Same as above, but if abbreviate-flag is non-NIL, then do not display commands between ``matching bookends''. See documentation for comm for an explanation of matching bookends.

Note: If there are more than n instructions in the state-stack, then (commands n) is the same as commands (and also, (commands n abb) is the same as (commands nil abb)).