LP, the Larch Prover -- The display-mode setting

The display-mode setting controls the manner in which the display command outputs identifiers and terms.

Syntax

<set-display-command> ::= set display-mode <qualification-mode>
<qualification-mode>  ::= qualified | unambiguous | unqualified
Note: The <qualification-mode> can be abbreviated.

Examples

set display-mode qualified

Usage

The display-mode setting controls the ouput of identifiers and terms by the display command in the current proof context. 
display-mode       effect
------------       ------
qualified          print qualifications for all subterms, identifiers
unqualified        print no qualifications
unambiguous        print enough qualifications to enable reparsing
The default display-mode is unambiguous.

See also