LP, the Larch Prover -- The resume command

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

Syntax

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

Examples

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

Usage

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