| | | B.2.3 prev, next: Cycle Through Open Proof States |
prev
next
: prev
: next
In proving mode.
All open proof states are internally organized in a list in an order as they are encountered by a depth-first left-to-right traversal of the proof tree. The command next switches the current state to its successor in the list (to the first state in the list, if the current state is the last one); the command prev switches the current state to its predecessor in the list (to the last state in the list, if the current state is the first one). Thus repeated applications of next respectively prev cycle through all open proof states.
To quickly switch to an open state distant from the current one, use the command goto respectively double-click on the corresponding item in the visual representation of the proof tree.
| | | B.2.3 prev, next: Cycle Through Open Proof States |