6.2 Navigation in the proof tree
6.2.1 Undo.
This command cancels the effect of the last tactic command. Thus, it backtracks one step.Error messages:
- No focused proof (No proof-editing in progress)
- Undo stack would be exhausted
Variants:
-
Undo num.
Repeats Undo num times.
6.2.2 Set Undo num.
This command changes the maximum number of Undo's that will be possible when doing a proof. It only affects proofs started after this command, such that if you want to change the current undo limit inside a proof, you should first restart this proof.6.2.3 Unset Undo.
This command resets the default number of possible Undo commands (which is currently 12).6.2.4 Restart.
This command restores the proof editing process to the original goal.Error messages:
- No focused proof to restart
6.2.5 Focus.
Will focus the attention on the first subgoal to prove, the remaining subgoals will no more be printed after the application of a tactic. This is useful when there are many current subgoals which clutter your screen.6.2.6 Unfocus.
Turns off the focus mode.