Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-04-01 23:45:26 -0800 (Mon, 01 Apr 2002)
Revision: 3553
Log message:

      1. Added "eqG" to the definition of groups which denotes the equivalence
         relation related with the group. Every group has an equivalence
         relation, which is now explicitly described.
      2. Accordingly, all rules related with equivalence relations in groups
         are updated and reproved.
      3. Added tactics "uniqueInvLeftT" and "uniqueInvRightT" which might not
         be very useful though.
      

Changes  Path
+121 -132 metaprl/theories/czf/czf_itt_group.ml
+11 -6 metaprl/theories/czf/czf_itt_group.mli
+5698 -5156 metaprl/theories/czf/czf_itt_group.prla