Note: Each <default-proof-method> can be abbreviated.
Examples
set proof =>, normalization
Usage
The set proof-methods command provides a list of default proof methods for
the current proof context. LP uses the first method in the list that applies
to the conjecture. The default list is normalization. Any method (other
than contradiction) that does not mention a variable or constant can
appear on the list. If the proof-method list is explicit-commands, then
LP will await a resume command before beginning the proof.