Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-03-11 01:57:12 -0800 (Mon, 11 Mar 2002)
Revision: 3534
Log message:

      1. Minor changes in the introduction rule for equivalence relations;
      2. Added tactics "equivSym1T" and "equivTrans1T" for the symmetry and
         transitivity of equivalence relations which are supposed to be
         applied to goals while "equivSymT" and "equivTransT" in the previous
         versions are supposed to be applied to hypotheses;
      3. Added the property that if 'a = 'b then 'a is equivalent to 'b under
         any equivalence relation;
      4. Added in comments the property that if 'a is equivalent to 'b under
         any equivalence relation then 'a = 'b. (This is not proved since I
         don't know how to express the set
         {(a, b): mem{'a; 's}, mem{'b; 's}, equal{'a; 'b}}.)
      

Changes	Path
+60 -4	metaprl/theories/czf/czf_itt_equiv.ml
+2 -0	metaprl/theories/czf/czf_itt_equiv.mli
+11919 -10937	metaprl/theories/czf/czf_itt_equiv.prla