LP, the Larch Prover -- The cancel command

The cancel command enables users to abort proofs or to change proof methods.


<cancel-command> ::= cancel [ all | lemma ]


cancel all
cancel lemma


The cancel command without either modifier cancels the proof of the current conjecture and suspends work on other proofs until an explicit
resume command is issued. If the current conjecture is a subgoal for proving a formula, LP pops the proof stack back to the parent of the subgoal and sets its proof method to default; if it is a subgoal for a nonformula (e.g., for an induction rule), LP also cancels the proof of the parent of the subgoal.

The command cancel all cancels the proofs of all conjectures.

The command cancel lemma cancels the proof of the conjecture introduced by the last prove command, together with the proofs of all subgoals introduced by LP during the proof of that conjecture.