LP, the Larch Prover -- The resume command
The resume command allows the user to resume work on the current
<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.