LP, the Larch Prover -- The resume command

The resume command allows the user to resume work on the current conjecture.


<presume-command> ::= resume [ by <proof-method> ]


resume by induction on i
resume by cases x < 0, x = 0, x > 0


The resume command resumes work on the current conjecture using the specified method. If no method is specified, LP uses the method in effect when the proof was suspended.

See also