Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-06-28 13:52:56 -0700 (Thu, 28 Jun 2001)
Revision: 3300
Log message:
- I moved the rule quotientElimination2 to the Itt_pointwise2, since it is
valid only for the pointwise functionality. Now this rule is derived
from Itt_pointwise.
I also proved t/bunionElimination2. Also I prove new versions of these rules
(t/bunion/quotientElimination_eq) that are stronger that weak eliminations,
but still valid in any functionality.
- I also moved the Eta reduction to a separate theory.
- I fixed and proved two rules in Itt_union.