| | | B.2.2 quit: Leave Current Mode |
quit
In declaration mode and in proving mode.
If in declaration mode, the command lets the system terminate. If in proving mode, the command asks the user whether to retain any original proof or to overwrite it with the newly constructed proof and then switches from proving mode back to declaration mode.
A proof is only saved to file when the command quit is executed (in proving mode).
The item "Quit" in window menu "File" and the window button "close" terminate the system, even when in proving mode, after confirmation by the user.
| | | B.2.2 quit: Leave Current Mode |