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

      1. Changed the definition of cyclic subgroups from cyclic_subgroup{'g;
         'a} to cyc_subg{'g; 's; 'a} where 's was added to represent the group
         of the cyclic_subgroup itself;
      2. Added the functionality (both equality and equivalence) of the "power"
         operation;
      3. Updated the properties of the power operation from "equal" to "equiv";
      4. Updated and proved rules about cyclic subgroups;
      5. Added tactic "cycsubgSubgroupT".
      
      Problem:
        czf_itt_cyclic_subgroup.prla could not be committed. It gave the message
         "cvs server: sticky tag `1.5' for file `czf_itt_cyclic_subgroup.prla'
          is not a branch".
      

Changes	Path
+70 -49	metaprl/theories/czf/czf_itt_cyclic_subgroup.ml
+5 -4	metaprl/theories/czf/czf_itt_cyclic_subgroup.mli