ELIM-DEFNS : FLAGELIM-DEFNS is a flag or parameter.
When printing a wff, first instantiate all of the definitions
and lambda-normalize. This instantiation will ignore REWRITE-DEFNS, but
will use the current setting of REWRITE-EQUALITIES.
It's best to leave this at NIL (i.e. off), since output with it set to T can
ELIM-DEFNS takes values of type BOOLEAN.
It belongs to subjects LIBRARY PRINTING .
Its default value is NIL
Its current value is NIL.
TPS documentation homepage