# 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` ]

## Examples

`cancel
cancel all
cancel lemma
`

## Usage

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.