Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-04-14 00:53:33 -0700 (Mon, 14 Apr 2003)
Revision: 4426
Log message:

      Defined group monomorphism/epimorphism; Changed the definition of group
      isomorphism; And added/proved more properties.
      
      Now everything about groups in CZF is implemented in ITT except the example
      of Klein 4-group.
      
      "groupMono_ker2" remains unproved since it requires some esquash equality
      elimination.
      

Changes  Path
+38 -0 metaprl/theories/itt/itt_comment.ml
+4 -0 metaprl/theories/itt/itt_comment.mli
+177 -69 metaprl/theories/itt/itt_group.ml
+4 -0 metaprl/theories/itt/itt_group.mli
+6935 -3469 metaprl/theories/itt/itt_group.prla
+1 -1 metaprl/theories/itt/itt_grouplikeobj.ml