Major Section: PROOF-TREE-EMACS
The key bindings set up when you start proof trees are shown below. See proof-tree-emacs for how to get started with proof trees.
C-z h help C-z ? helpProvides information about proof-tree/checkpoint tool. Use `C-h d' to get more detailed information for specific functions.
C-z c Go to checkpointGo to a checkpoint, as displayed in the "prooftree" buffer with the character
cin the first column. With non-zero prefix argument: move the point in the ACL2 buffer (emacs variable
*mfm-buffer*) to the first checkpoint displayed in the "prooftree" buffer, suspend the proof tree (see
suspend-proof-tree), 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.
If the prefix argument is 0, move to the first checkpoint but do not keep suspended.
C-z g Goto subgoalGo to the specified subgoal in the ACL2 buffer (emacs variable
*mfm-buffer*) 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.
C-z r Resume proof treeResume original proof tree display, re-creating buffer "prooftree" if necessary. See also
suspend-proof-tree. With prefix argument: push the mark, do not modify the windows, and move point to end of
C-z s Suspend proof treeFreeze the contents of the "prooftree" buffer, until
resume-proof-treeis invoked. Unlike
stop-proof-tree, the only effect of
suspend-proof-treeis 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
C-z o Select other frame C-z b Switch to "prooftree" buffer C-z B Switch to frame called "prooftree-frame"These commands move between buffers and frames, as indicated. The first of these has nothing specifically to do with proof trees, but is handy if you have at least two emacs frames displayed. The second takes you to the "prooftree" buffer (in the current frame), while the third takes you to the frame called "prooftree-frame", creating it if it does not already exist.