Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-05-09 04:44:01 -0700 (Fri, 09 May 2003)
Revision: 4577
Log message:

       - Added extentional group equality.
       - Proved some (somewhat) complicated theorems about quotient groups.
      

Changes  Path
+48 -5 metaprl/theories/itt/itt_group.ml
+3 -0 metaprl/theories/itt/itt_group.mli
+9125 -7782 metaprl/theories/itt/itt_group.prla
+31 -3 metaprl/theories/itt/itt_quotient_group.ml
+5564 -1325 metaprl/theories/itt/itt_quotient_group.prla