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.

DIAG

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

LONG DIAG

Has the same effect as four DIAG s.

LONG LONG DIAG

Sets the current node to be the root of the proof. The cursor will point to the environment of its goal.

LONG

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.