Next: Initiating a Refinement
Up: The Proof Editor
Previous: Motion within a
The following commands allow one to move around within the proof.
They change the current node by moving into or out of subproofs.
Any other combination of LONG
and the arrow keys is ignored.
s are ignored.
Only has an effect when the cursor is in a subgoal;
the node for that subgoal becomes the current node.
Sets the current node to be the parent of the current node.
The cursor will still point to the current goal, but the current goal
will be displayed as one of the subgoals of the parent.
If the cursor isn't in the goal DIAG
} moves it to point to
the goal. If it is in the goal, the parent of the current node will
become the new current node, (as in
) and the cursor will point to
its goal (unlike
Has the same effect as four DIAG
Sets the current node to be the root of the proof.
The cursor will point to the environment of its goal.
Sets the current node to be the next unproved node of the proof tree.
The search is done in preorder and wraps around the tree if necessary.
If the proof has no incomplete nodes the current node is set to be the
Thu Sep 14 08:45:18 EDT 1995