functions that display or change history
Major Section:  ACL2 Documentation

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.