Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-03-10 02:03:15 -0800 (Mon, 10 Mar 2003)
Revision: 4161
Log message:

       - Proved some properties of group homomorphism.
         "Membership is a type iff it is true" also causes problems in proving
         "If f:A->B is a homomorphism and T is is a subgroup of B, then the
          inverse image of T under f is a subgroup of A", as in
          "/itt_group/groupHom_subg2/2" and "/itt_group/groupHom_subg2/3".
      
       - Uncommented some reduce resources in itt_int_ext.
      
       - Added several theorems about grouplikeobj and groups.
      

Changes  Path
+171 -233 metaprl/theories/itt/itt_cyclic_group.prla
+113 -15 metaprl/theories/itt/itt_group.ml
+5563 -1578 metaprl/theories/itt/itt_group.prla
+6 -0 metaprl/theories/itt/itt_grouplikeobj.ml
+340 -228 metaprl/theories/itt/itt_grouplikeobj.prla
+7 -9 metaprl/theories/itt/itt_int_ext.ml
+4804 -3718 metaprl/theories/itt/itt_int_ext.prla