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

      1. Replaced equality relations with equivalence relations in
         the definition axioms for "op", "inv", and "id".
      2. Defined the equivalence functionality for "op" and "inv".
      3. Changed the tactics for "left and right cancellation laws"
         (i.e., groupCancelLeftT and groupCancelRightT) to make it
         easier to use.
      4. Re-proved all properties.
      

Changes	Path
+82 -407	metaprl/theories/czf/czf_itt_group.ml
+4 -2	metaprl/theories/czf/czf_itt_group.mli
+4640 -3562	metaprl/theories/czf/czf_itt_group.prla