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 |