functions that display or change history
Parent topic: Home
OOPS -- undo a :u or :ubt
PBT -- print the commands back through a command descriptor
PC -- print the command described by a command descriptor
PCB -- print the command block described by a command descriptor
PCB! -- print in full the command block described by a command descriptor
PCS -- print the sequence of commands between two command descriptors
PE -- print the event named by a logical name
PE! -- print all the events named by a logical name
PF -- print the formula corresponding to the given name
PL -- print the rules whose top function symbol is the given name
PR -- print the rules stored by the event with the given name
PR! -- print rules stored by the command with a given command descriptor
PUFF -- replace a compound command by its immediate subevents
PUFF* -- replace a compound command by its subevents
U -- undo last command, without a query
UBT -- undo the commands back through a command descriptor
UBT! -- undo commands, without a query or an error
ACL2 keeps track of the commands that you have executed that have
extended the logic or the rule data base, as by the definition of
macros, functions, etc. Using the facilities in this section you
can review the sequence of commands executed so far. For example,
you can ask to see the most recently executed command, or the
command 10 before that, or the command that introduced a given
function symbol. You can also undo back through some previous
command, restoring the logical world to what it was before the given
command.
The annotations printed in the margin in response to some of these
commands (such as `P', `L', and `V') are explained in the
documentation for :pc.
Several technical terms are used in the documentation of the history
commands. You must understand these terms to use the commands.
These terms are documented via :doc entries of their own.
See command, see events, see command-descriptor, and
see logical-name.