Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-03-24 03:01:50 -0800 (Sun, 24 Mar 2002)
Revision: 3549
Log message:

      1. The original equivTransT was wrong. Changed the original equivTrans1T
         and equivSym1T into equivTransT and equivSymT; Changed the original
         equivSymT to equivSym1T and removed equivTrans1T.
      2. Added the "fold" form for "equiv".
      3. Reproved rules in the file.
      

Changes  Path
+34 -40 metaprl/theories/czf/czf_itt_equiv.ml
+15 -7 metaprl/theories/czf/czf_itt_equiv.mli
+9461 -13172 metaprl/theories/czf/czf_itt_equiv.prla