Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-03-07 15:13:10 -0800 (Thu, 07 Mar 2002)
Revision: 3530
Log message:

      1. Added properties that "e * a = a * e" and "a * e = e * a".
      2. Changed the definition of groups to one-sided (left) definition,
         i.e., groups are defined by the left axioms, and proved the right
         axioms.
      3. Removed the introduction forms of group cancellation laws which
         were put in comments in the last version.
      

Changes	Path
+40 -45	metaprl/theories/czf/czf_itt_group.ml
+1493 -774	metaprl/theories/czf/czf_itt_group.prla