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
|
<html>
<head><title>PROOF-TREE-BINDINGS.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h3>PROOF-TREE-BINDINGS</h3>using emacs with proof trees
<pre>Major Section: <a href="PROOF-TREE-EMACS.html">PROOF-TREE-EMACS</a>
</pre><p>
The key bindings set up when you start proof trees are shown below.
See <a href="PROOF-TREE-EMACS.html">proof-tree-emacs</a> for how to get started with proof trees.
<p>
<pre>
C-z h help
C-z ? help
</pre>
Provides information about proof-tree/checkpoint tool.
Use `C-h d' to get more detailed information for specific functions.<p>
<pre>
C-z c Go to checkpoint
</pre>
Go to a checkpoint, as displayed in the "prooftree" buffer with
the character <code>c</code> in the first column. With non-zero prefix
argument: move the point in the ACL2 buffer (emacs variable
<code>*mfm-buffer*</code>) to the first checkpoint displayed in the "prooftree"
buffer, suspend the proof tree (see <code>suspend-proof-tree</code>), and move the
cursor below that checkpoint in the "prooftree" buffer. Without a
prefix argument, go to the first checkpoint named below the point in
the "prooftree" buffer (or if there is none, to the first
checkpoint). Note however that unless the proof tree is suspended or
the ACL2 proof is complete or interrupted, the cursor will be
generally be at the bottom of the "prooftree" buffer each time it is
modified, which causes the first checkpoint to be the one that is
found.<p>
If the prefix argument is 0, move to the first checkpoint but do not
keep suspended.<p>
<pre>
C-z g Goto subgoal
</pre>
Go to the specified subgoal in the ACL2 buffer (emacs variable
<code>*mfm-buffer*</code>) that lies closest to the end of that buffer -- except if
the current buffer is "prooftree" when this command is invoked, the
subgoal is the one from the proof whose tree is displayed in that
buffer. A default is obtained, when possible, from the current line
of the current buffer.
<pre>
C-z r Resume proof tree
</pre>
Resume original proof tree display, re-creating buffer
"prooftree" if necessary. See also <code>suspend-proof-tree</code>. With prefix
argument: push the mark, do not modify the windows, and move point to
end of <code>*mfm-buffer*</code>.<p>
<pre>
C-z s Suspend proof tree
</pre>
Freeze the contents of the "prooftree" buffer, until
<code>resume-proof-tree</code> is invoked. Unlike <code>stop-proof-tree</code>, the only effect
of <code>suspend-proof-tree</code> is to stop putting characters into the
"prooftree" buffer; in particular, strings destined for that buffer
continue NOT to be put into the primary buffer, which is the value of
the emacs variable <code>*mfm-buffer*</code>.
<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>
|
