Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-14 14:32:24 -0700 (Sat, 14 Jul 2001)
Revision: 3331
Log message:
- The Itt_quotient theory is now a theory of _intensional_ quotient type
(one can still get extensional one by esquash'ing the equality predicate).
- Most of the Itt_quotient theory rules are now reversible.