TIMING-NAMED : FLAGTIMING-NAMED is a flag or parameter.
If T, the labels printed by display-time will be shortened
to allow room for the name of the current dproof, if there is one.
If NIL, then they won't.
Abbreviations used are: PRE - preprocessing, MS - mating search,
U - unification, PPR - postprocessing, MRG - merging,
TRA - translation, PRT - printing.
TIMING-NAMED takes values of type BOOLEAN.
It belongs to subjects MATING-SEARCH SYSTEM .
Its default value is NIL
Its current value is T.
TPS documentation homepage