The keyboard commands for moving about proofs are summarized in
Table 
. The commands closely match a subset of
the term editor motion commands (described in
Section ). A part of the window is a
either a goal sequent, a refinement rule, a rule placeholder or a
subgoal.
The FORWARD-PART and BACK-PART commands move the cursor within a proof window from part to part, if necessary scrolling the window. FIRST-PART moves the cursor to the goal and LAST-PART moves the cursor to the last subgoal if there are any subgoals; otherwise it moves the cursor to the refinement rule part.
The UP-TO-PARENT command, executed with a cursor in any part of the window, shifts the window one level up the proof tree. DOWN-TO-CHILD, executed with the cursor over a subgoal part, shifts the window down the proof tree to that subgoal. The NEXT-UNREFINED-LEAF command shifts the window to the next unrefined proof node in a preorder traversal of the proof tree. If there are none, NEXT-UNREFINED-LEAF shifts the window to the root of the proof.
The mouse can also be used to move about a proof. See
Section for details. Most users find
these easier to use than the key bindings.
