Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-02-24 21:51:45 -0800 (Mon, 24 Feb 2003)
Revision: 4122
Log message:

      1. Added display forms for the terms.
      2. Separate commutative semigroup/monoid and abelian group from the
         grouplikeobj/group modules.
      
      Any comment on the display forms?
      

Changes	Path
+1 -0	metaprl/theories/itt/Makefile
Added	metaprl/theories/itt/itt_abelian_group.ml
Properties	metaprl/theories/itt/itt_abelian_group.ml
Added	metaprl/theories/itt/itt_abelian_group.mli
Properties	metaprl/theories/itt/itt_abelian_group.mli
Added	metaprl/theories/itt/itt_abelian_group.prla
Properties	metaprl/theories/itt/itt_abelian_group.prla
+111 -0	metaprl/theories/itt/itt_comment.ml
+16 -0	metaprl/theories/itt/itt_comment.mli
+9 -17	metaprl/theories/itt/itt_group.ml
+4 -2	metaprl/theories/itt/itt_group.mli
+1993 -2291	metaprl/theories/itt/itt_group.prla
+17 -38	metaprl/theories/itt/itt_grouplikeobj.ml
+0 -8	metaprl/theories/itt/itt_grouplikeobj.mli
+1789 -2579	metaprl/theories/itt/itt_grouplikeobj.prla