HISTORY

Major Section:  ACL2 Documentation

Some Related Topics

• GCS -- See get-command-sequence.

• GET-COMMAND-SEQUENCE -- return list of commands that are between two command descriptors

• 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 events named by a logical name

• PE! -- deprecated (see pe)

• PF -- print the formula corresponding to the given name

• PL -- print the rules for the given name or term

• PL2 -- print rule(s) for the given form

• 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

• RESET-KILL-RING -- save memory by resetting and perhaps resizing the kill ring used by oops

• TAU-DATA -- to see what tau knows about a function symbol

• TAU-DATABASE -- to see the tau database as a (very large) object

• 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

• UBT-PREHISTORY -- undo the commands back through the last reset-prehistory event

• UBU -- undo the commands back up to (not including) a command descriptor

• UBU! -- 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 database, 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.