LP, the Larch Prover — The automatic-ordering setting
The automatic-ordering setting controls whether LP orients formulas into
rewrite rules with or without the user having to issue an explicit
order command.
<set-automatic-ordering-command> ::= set automatic-ordering ( on | off )
Examples
set auto-ord off
Usage
If automatic-ordering is on (the default), then LP attempts to orient
all formulas (asserted axioms, proved conjectures, results of deductions,
instantiations, critical pair equations, and hypotheses for subgoals in proofs)
automatically into rewrite rules. If it is off, then the user must issue
an explicit order command to orient formulas into rewrite rules. The
value of this setting is local to the current proof context.