We first make the following definitions. The proof cursor is in a goal if it points to a hypothesis or the conclusion; it is at a goal if it points to the first part of the goal. If the cursor is not in a goal, it is at the rule of the current node or in or at a subgoal.
The cursor can be moved around within the current proof node in the following ways:
, 
Moves the cursor up or down to the next or previous minor stopping point. A minor stopping point is an assumption, a conclusion or the rule.
, LONG
Moves the cursor up or down to the next or previous major stopping point. A major stopping point is a subgoal, a rule or the goal.
Moves the cursor to the goal.
Moves the cursor to the conclusion of the last subgoal.