Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-02-05 00:20:00 -0800 (Tue, 05 Feb 2002)
Revision: 3491
Log message:

      Proved all rules related to the properties of cyclic subgroups.
      
      TODO:
         rule lt_Id and tactic lt_IdT are better to be moved into module "itt_int_base" upon Yegor's approval.
      

Changes  Path
+7 -0 metaprl/theories/czf/czf_itt_cyclic_subgroup.ml
+5 -0 metaprl/theories/czf/czf_itt_cyclic_subgroup.mli
+1883 -714 metaprl/theories/czf/czf_itt_cyclic_subgroup.prla