		Search-engine friendly clone of the ACL2 documentation.

Proof-builder-commands

ACL2-pc::commands

(macro) display instructions from the current interactive session

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.

Remark: 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)).