CHANGE-PRINT-TYPE : WFFOPCHANGE-PRINT-TYPE is a wff operation.
Use the type specified whenever this symbol is printed. Note that
this type may be overridden, if the flag retain-initial-type is NIL.
The calling scheme for CHANGE-PRINT-TYPE is:
(CHANGE-PRINT-TYPE GVAR TYPESYM)
The result is of type TYPESYM.
The arguments have the following meaning:
GVAR : Symbol
TYPESYM : Type to be used for printing
TPS documentation homepage