LP, the Larch Prover -- The cancel command
The cancel command enables users to abort proofs or to change proof
<cancel-command> ::= cancel [ all | 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.