Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-01-29 16:36:09 -0800 (Tue, 29 Jan 2002)
Revision: 3484
Log message:

      Now a workable version for groups and cyclic subgroups. Rules proved, examples  added.
      Problems left:
         The proofs for rules "power_property1", "power_property2", and "power_simplify" are not yet finished because of some itt problems.
      

Changes  Path
+24 -8 metaprl/theories/czf/czf_itt_cyclic_subgroup.ml
+4359 -1015 metaprl/theories/czf/czf_itt_cyclic_subgroup.prla
+21 -17 metaprl/theories/czf/czf_itt_group.ml
+1226 -930 metaprl/theories/czf/czf_itt_group.prla