History
Functions to display or change contents of the logical world
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 (by issuing :pc :x), or the
preceding 10 commands (by issuing :pbt :x-10), or the
command that introduced a given function symbol, fn (by issuing :pc
fn). You can also undo back through some previous command (see ubt),
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
(including `P', `L', `V', `D', `d', 'M', and 'm') 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 with documentation entries of their own. See command, see events, see command-descriptor, and see logical-name.
Subtopics
- Pl
- Print the rules for the given name or term
- Command
- Forms you type at the top-level, but...
- Puff
- Replace a compound command by its immediate subevents
- Pc
- Print the command described by a command descriptor
- Ld-history
- Saving and querying command history
- Oops
- Undo a :u or :ubt
- Extend-pe-table
- Replace events displayed by history commands
- Ubt
- Undo the commands back through a command descriptor
- Puff*
- Replace a compound command by its subevents
- Ubi
- Undo back up to longest initial segment containing only calls of
certain symbols, including defpkg and include-book.
- Undo
- Undoing and perhaps redefining
- Pe
- Print the events named by a logical name
- Make-termination-theorem
- Create a copy of a function's termination theorem that calls stubs.
- Command-descriptor
- An object describing a particular command typed by the user
- Reset-prehistory
- Reset the prehistory
- Gthm
- The guard theorem for a given function symbol
- Formula
- The formula of a name or rune
- Pr
- Print the rules stored by the event with the given name
- Pcb
- Print the command block described by a command descriptor
- Ubu
- Undo the commands back up to (not including) a command descriptor
- Disable-ubt
- Make it illegal to undo back through the current command
- Pl2
- Print rule(s) for the given form
- Pbt
- Print the commands back through a command descriptor
- Enter-boot-strap-mode
- The first millisecond of the Big Bang
- Reset-kill-ring
- Save memory by resetting and perhaps resizing the kill ring used by oops
- Ubt!
- Undo commands, without a query or an error
- U
- Undo last command, without a query
- Tthm
- The measure (termination) theorem for a given function symbol
- Pf
- Print the formula corresponding to the given name
- Ubu!
- Undo commands, without a query or an error
- Pr!
- Print rules stored by the command with a given command descriptor
- Pcs
- Print the sequence of commands between two command descriptors
- Pcb!
- Print in full the command block described by a command descriptor
- Get-command-sequence
- Return list of commands that are between two command descriptors
- Exit-boot-strap-mode
- The end of pre-history
- Ubu?
- Undo commands, with queries as appropriate
- Ubt?
- Undo commands, with queries as appropriate
- Ep-
- Return the sorted list of non-builtin event names matching a given
prefix
- Ubt-prehistory
- Undo the commands back through the last reset-prehistory event
- Tau-database
- To see the tau database as a (very large) object
- Ep
- Return the sorted list of event names matching a given prefix
- Pe!
- Print events as with pe but ignoring the pe-table
