Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-26 03:22:43 -0700 (Sun, 26 May 2002)
Revision: 3693
Log message:

      Changed the definition of the carrier in cyclic subgroups/groups from
      collection to separation. The reason for this is that we should always
      try to use set primitives rather than collections.
      Updated corresponding rules and proofs.
      Also made some minor changes in comments.
      

Changes  Path
+9 -16 metaprl/theories/czf/czf_itt_cyclic_group.ml
+1 -1 metaprl/theories/czf/czf_itt_cyclic_group.mli
+2617 -2779 metaprl/theories/czf/czf_itt_cyclic_group.prla
+20 -6 metaprl/theories/czf/czf_itt_cyclic_subgroup.ml
+1 -1 metaprl/theories/czf/czf_itt_cyclic_subgroup.mli
+2499 -1928 metaprl/theories/czf/czf_itt_cyclic_subgroup.prla
+1 -1 metaprl/theories/czf/czf_itt_group.ml
+3 -3 metaprl/theories/czf/czf_itt_group_power.ml
+19 -15 metaprl/theories/czf/czf_itt_hom.ml
+25 -24 metaprl/theories/czf/czf_itt_ker.ml
+1123 -1126 metaprl/theories/czf/czf_itt_ker.prla
+1 -0 metaprl/theories/czf/czf_itt_kleingroup.ml
+1 -1 metaprl/theories/czf/czf_itt_subgroup.ml