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 )


set auto-ord off


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.