next up previous contents index
Next: Initiating a Refinement Up: The Proof Editor Previous: Motion within a

Motion within the Proof Tree

  The following commands allow one to move around within the proof. They change the current node by moving into or out of subproofs.

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 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 s.


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 root.

LONG } Any other combination of LONG and the arrow keys is ignored. Extra LONG s are ignored.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995