LP, the Larch Prover -- Proofs by explicit commands

The special proof method explicit-commands 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 time-consuming 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.