Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-03-03 16:45:01 -0800 (Mon, 03 Mar 2003)
Revision: 4151
Log message:

      - Defined subset, subStructure (which can be used for semigroup, monoid,
        group, etc.), cyclic group (including the power operation for a group
        and cyclic subgroups); and proved corresponding theorems.
      - Adopted Alexei's new syntax.
      - Removed "itt_abelian_group" module, and moved "isCommutative" to "itt_
        grouplikeobj".
      
      Note: The subset module is rather incomplete. It only includes what I
      currently will use.
      

Changes  Path
+3 -2 metaprl/theories/itt/Makefile
+91 -0 metaprl/theories/itt/itt_comment.ml
+11 -0 metaprl/theories/itt/itt_comment.mli
Added metaprl/theories/itt/itt_cyclic_group.ml
Properties metaprl/theories/itt/itt_cyclic_group.ml
Added metaprl/theories/itt/itt_cyclic_group.mli
Properties metaprl/theories/itt/itt_cyclic_group.mli
Added metaprl/theories/itt/itt_cyclic_group.prla
Properties metaprl/theories/itt/itt_cyclic_group.prla
+269 -50 metaprl/theories/itt/itt_group.ml
+3 -0 metaprl/theories/itt/itt_group.mli
+7842 -2655 metaprl/theories/itt/itt_group.prla
+31 -8 metaprl/theories/itt/itt_grouplikeobj.ml
+4 -0 metaprl/theories/itt/itt_grouplikeobj.mli
+2146 -1683 metaprl/theories/itt/itt_grouplikeobj.prla
Added metaprl/theories/itt/itt_subset.ml
Properties metaprl/theories/itt/itt_subset.ml
Added metaprl/theories/itt/itt_subset.mli
Properties metaprl/theories/itt/itt_subset.mli
Added metaprl/theories/itt/itt_subset.prla
Properties metaprl/theories/itt/itt_subset.prla