Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-02-21 00:29:40 -0800 (Fri, 21 Feb 2003)
Revision: 4104
Log message:

      - Defined group like objects: groupoid, semigroup, and monoid with dependent
        records.
      - Defined groups based on the definitions of group like objects with
        dependent records.
      - Proved all properties in CZF for groups here in ITT.
      
      TODO:
      1. Might simplify the display forms of "*" later.
      2. Might need more research on using constants as field names.
      3. After the rewriter bug is fixed, some proofs might be simplified and the
         elimination rules for groups etc. are unnecessary.
      

Changes	Path
+2 -0	metaprl/theories/itt/Makefile
Added	metaprl/theories/itt/itt_group.ml
Properties	metaprl/theories/itt/itt_group.ml
Added	metaprl/theories/itt/itt_group.mli
Properties	metaprl/theories/itt/itt_group.mli
Added	metaprl/theories/itt/itt_group.prla
Properties	metaprl/theories/itt/itt_group.prla
Added	metaprl/theories/itt/itt_grouplikeobj.ml
Properties	metaprl/theories/itt/itt_grouplikeobj.ml
Added	metaprl/theories/itt/itt_grouplikeobj.mli
Properties	metaprl/theories/itt/itt_grouplikeobj.mli
Added	metaprl/theories/itt/itt_grouplikeobj.prla
Properties	metaprl/theories/itt/itt_grouplikeobj.prla