Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-07-06 13:02:02 -0700 (Fri, 06 Jul 2001)
Revision: 3318
Log message:
- Fixed some bugs in Itt_w:
(a) The rule ruduce_tree_eta was unsound (we could prove unconditional
eta from it). Removed
(b) The rule wElimination was also unsound. Fixed.
(c) There old bug noticed by Carl 2 years ago survived in the rule
tree_indEquality. I fixed this rule, make it more general,
make it interacative instead of primitive and proved it.
- Display forms for srec and prec types are fixed.