save queries the user and is answered negatively, then the exit
is aborted.
exit after possibly saving the state
Major Section: PROOF-CHECKER-COMMANDS
Example and General Form: ex
Same as exit, except that first the instruction save is executed.
If save queries the user and is answered negatively, then the exit
is aborted.