PRINT-UNTIL-UI-OR-EGEN : FLAGPRINT-UNTIL-UI-OR-EGEN is a flag or parameter.
When set to t, the commands PBRIEF and EXPLAIN will
continue to print beyond the depth specified until a line justified
by UI or Egen is encountered. The intuition is that these are
the real choice points in the proof. When set to nil, PBRIEF
and EXPLAIN print only to the depth specified.
PRINT-UNTIL-UI-OR-EGEN takes values of type BOOLEAN.
It belongs to subjects PRINTING .
Its default value is NIL
Its current value is NIL.
TPS documentation homepage