REMOVE-LEIBNIZ is a flag or parameter.
If TRUE, selection parameters corresponding to Leibniz equality
definitions will be removed from expansion proofs during merging
(cf. Pfenning's thesis, theorem 138).
REMOVE-LEIBNIZ takes values of type BOOLEAN.
It belongs to subjects MS93-1 MS92-9 MS91-7 MS91-6 MS90-9 MS90-3 MS89 MS88 ETR-NAT ETREES MATING-SEARCH .
Its default value is T
Its current value is T.

TPS documentation homepage

© 1988-99, Carnegie Mellon University.

TPS homepage