Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-08-05 18:52:46 -0700 (Wed, 05 Aug 1998)
Revision: 2412
Log message:
Fixed unification to compare constants after bound variables,
and to unify constants like other terms. Fixed a problem with
bound variable naming in hypothesis rewriting. TPTP quantifiers
are over atom0.
Finally, terms that are equal may not be alpha-equal. Never assume
that ordinary equality (=) on terms has any logical meaning. Fixed
equality bug on xnil_term in TermMan.