1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
|
<html>
<head><title>HISTORY.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h1>HISTORY</h1>functions that display or change history
<pre>Major Section: <a href="acl2-doc-major-topics.html">ACL2 Documentation</a>
</pre><p>
<p>
<ul>
<li><h3><a href="OOPS.html">OOPS</a> -- undo a <code>:u</code> or <code>:</code><code><a href="UBT.html">ubt</a></code>
</h3>
</li>
<li><h3><a href="PBT.html">PBT</a> -- print the <a href="COMMAND.html">command</a>s back through a <a href="COMMAND.html">command</a> descriptor
</h3>
</li>
<li><h3><a href="PC.html">PC</a> -- print the <a href="COMMAND.html">command</a> described by a <a href="COMMAND.html">command</a> descriptor
</h3>
</li>
<li><h3><a href="PCB.html">PCB</a> -- print the <a href="COMMAND.html">command</a> block described by a <a href="COMMAND.html">command</a> descriptor
</h3>
</li>
<li><h3><a href="PCB_bang_.html">PCB!</a> -- print in full the <a href="COMMAND.html">command</a> block described by a <a href="COMMAND.html">command</a> descriptor
</h3>
</li>
<li><h3><a href="PCS.html">PCS</a> -- print the sequence of <a href="COMMAND.html">command</a>s between two <a href="COMMAND.html">command</a> descriptors
</h3>
</li>
<li><h3><a href="PE.html">PE</a> -- print the events named by a logical name
</h3>
</li>
<li><h3><a href="PE_bang_.html">PE!</a> -- deprecated (see <a href="PE.html">pe</a>)
</h3>
</li>
<li><h3><a href="PF.html">PF</a> -- print the formula corresponding to the given name
</h3>
</li>
<li><h3><a href="PL.html">PL</a> -- print the rules for the given name or term
</h3>
</li>
<li><h3><a href="PR.html">PR</a> -- print the rules stored by the event with the given name
</h3>
</li>
<li><h3><a href="PR_bang_.html">PR!</a> -- print rules stored by the command with a given command descriptor
</h3>
</li>
<li><h3><a href="PUFF.html">PUFF</a> -- replace a compound <a href="COMMAND.html">command</a> by its immediate subevents
</h3>
</li>
<li><h3><a href="PUFF_star_.html">PUFF*</a> -- replace a compound <a href="COMMAND.html">command</a> by its subevents
</h3>
</li>
<li><h3><a href="RESET-KILL-RING.html">RESET-KILL-RING</a> -- save memory by resetting and perhaps resizing the kill ring used by <code><a href="OOPS.html">oops</a></code>
</h3>
</li>
<li><h3><a href="U.html">U</a> -- undo last <a href="COMMAND.html">command</a>, without a query
</h3>
</li>
<li><h3><a href="UBT.html">UBT</a> -- undo the <a href="COMMAND.html">command</a>s back through a <a href="COMMAND.html">command</a> descriptor
</h3>
</li>
<li><h3><a href="UBT_bang_.html">UBT!</a> -- undo <a href="COMMAND.html">command</a>s, without a query or an error
</h3>
</li>
<li><h3><a href="UBT-PREHISTORY.html">UBT-PREHISTORY</a> -- undo the <a href="COMMAND.html">command</a>s back through the last <code><a href="RESET-PREHISTORY.html">reset-prehistory</a></code> event
</h3>
</li>
<li><h3><a href="UBU.html">UBU</a> -- undo the <a href="COMMAND.html">command</a>s back up to (not including) a <a href="COMMAND.html">command</a> descriptor
</h3>
</li>
<li><h3><a href="UBU_bang_.html">UBU!</a> -- undo <a href="COMMAND.html">command</a>s, without a query or an error
</h3>
</li>
</ul>
ACL2 keeps track of the <a href="COMMAND.html">command</a>s 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 <a href="COMMAND.html">command</a>s executed so far. For example,
you can ask to see the most recently executed <a href="COMMAND.html">command</a>, or the
<a href="COMMAND.html">command</a> <code>10</code> before that, or the <a href="COMMAND.html">command</a> that introduced a given
function symbol. You can also undo back through some previous
<a href="COMMAND.html">command</a>, restoring the logical <a href="WORLD.html">world</a> to what it was before the given
<a href="COMMAND.html">command</a>.<p>
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 <code>:</code><code><a href="PC.html">pc</a></code>.<p>
Several technical terms are used in the documentation of the history
<a href="COMMAND.html">command</a>s. You must understand these terms to use the <a href="COMMAND.html">command</a>s.
These terms are documented via <code>:</code><code><a href="DOC.html">doc</a></code> entries of their own.
See <a href="COMMAND.html">command</a>, see <a href="EVENTS.html">events</a>, see <a href="COMMAND-DESCRIPTOR.html">command-descriptor</a>, and
see <a href="LOGICAL-NAME.html">logical-name</a>.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
