LP, the Larch Prover -- The automatic-registry setting
The automatic-registry setting controls whether LP asks the user to
confirm extensions to the registry when formulas are oriented into rewrite
rules.
<set-automatic-registry-command> ::= set automatic-registry ( on | off )
Examples
set auto-reg off
Usage
If automatic-registry is on (the default), then LP automatically
extends its registry, if necessary, when using a
registered ordering to orient formulas into
rewrite rules. If it is off, LP prompts the user to select one of a list
of possible extensions whenever the registry must be extended. When it is
off, LP also gives users the opportunity to divide
incompatible equations and to orient formulas
manually.