The completion-mode setting affects the order in which completion tasks
are executed in the current proof context. It also affects the amount of user
interaction during the completion procedure.
The standard mode (the default) computes
critical pair equations before extending
the registry. When the
automatic-registry setting is off, this reduces the amount of
interaction required from the user to extend the registry; however, it can be
inefficient.
The expert mode gives higher priority to orienting formulas into rewrite
rules than to computing critical pair equations. When the
automatic-registry setting is off, this gives the user more
explicit control over the completion process by prompting for guidance more
often. In particular, user interaction to order unordered formulas is
requested before the system attempts to compute new critical pairs.
The big mode postpones the computation of critical pairs even farther,
so that big formulas are examined before critical pairs are computed.