Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-03-11 02:04:22 -0800 (Mon, 11 Mar 2002)
Revision: 3538
Log message:

      1. Changed the definition of cyclic groups from cyclic_group{'g;'a}
         which represented the carrier set of the cyclic group to
         cycgroup{'g; 'a} which is a "type" and can be rewritted as
         cyc_subg{'g; 'g; 'a};
      2. Updated and proved rules about cyclic groups;
      3. Added tactic "cycgroupAbelT".
      

Changes	Path
+24 -43	metaprl/theories/czf/czf_itt_cyclic_group.ml
+5 -4	metaprl/theories/czf/czf_itt_cyclic_group.mli
+1548 -1195	metaprl/theories/czf/czf_itt_cyclic_group.prla