| | | B.2.1 prove: Enter Proving Mode |
prove F
In declaration mode.
The command takes the name F of a formula. If the formula already has an associated proof, the user is asked whether to enter this proof or to start a new proof. The system consequently switches to proving mode setting the current proof state to the first open state in the proof.
Before leaving the proving mode by the command quit, the user may decide whether to retain the proof originally associated to the formula or to overwrite it with the the newly constructed proof.
| | | B.2.1 prove: Enter Proving Mode |