B.2 Control Commands

B.2 Control Commands

The commands listed in this section do not alter the proof; they rather enable the user to enter or leave a proof, to navigate within a proof, and to get additional information on proof states.

• B.2.1 prove: Enter Proving Mode
• B.2.2 quit: Leave Current Mode
• B.2.3 prev, next: Cycle Through Open Proof States
• B.2.4 undo, redo: Undo/Redo Proof Commands
• B.2.5 goto: Go to Another Open Proof State
• B.2.6 counterexample: Generate Counterexample
• B.2.7 Abort Prover Activity
• B.2.8 state: Display Another Proof State
• B.2.9 open: List Open Proof States

B.2 Control Commands