LP, the Larch Prover  Proofs by explicit commands
The special proof method explicitcommands directs LP not to apply any
method of backward inference automatically to a conjecture, but to wait for an
explicit method to be given with a subsequent resume command. This
method is useful in several situations.

It can be used to prevent LP from attempting to normalize a conjecture when it
would be timeconsuming and unfruitful to do so. For example, if a conjecture
includes many conjuncts, it may be appropriate to first compute some critical
pairs, then apply the /\method, and finally normalize the individual
subgoals.

It can be used to delay the start of a proof until the user has had an
opportunity to make the conjecture immune, so that it is not reduced
once it has been proved.