Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-16 00:48:04 -0700 (Thu, 16 May 2002)
Revision: 3646
Log message:

      Defining groups does not really need equivalence relations, so I changed the group system by replacing equivalence relation with equality. Every occurance was modified and every related rule was reproved.
      
      Besides, separated the power operation for a group from the module Czf_itt_cyclic_subgroup.
      

Changes  Path
+1 -0 metaprl/theories/czf/Makefile
+2 -2 metaprl/theories/czf/czf_itt_abel_group.ml
+1 -1 metaprl/theories/czf/czf_itt_abel_group.mli
+2720 -2783 metaprl/theories/czf/czf_itt_abel_group.prla
+26 -37 metaprl/theories/czf/czf_itt_coset.ml
+3 -3 metaprl/theories/czf/czf_itt_coset.mli
+4661 -5820 metaprl/theories/czf/czf_itt_coset.prla
+3912 -3983 metaprl/theories/czf/czf_itt_cyclic_group.prla
+9 -114 metaprl/theories/czf/czf_itt_cyclic_subgroup.ml
+2 -7 metaprl/theories/czf/czf_itt_cyclic_subgroup.mli
+4310 -15346 metaprl/theories/czf/czf_itt_cyclic_subgroup.prla
+116 -171 metaprl/theories/czf/czf_itt_group.ml
+0 -5 metaprl/theories/czf/czf_itt_group.mli
+8760 -10938 metaprl/theories/czf/czf_itt_group.prla
+10 -18 metaprl/theories/czf/czf_itt_group_bvd.ml
+2 -4 metaprl/theories/czf/czf_itt_group_bvd.mli
+3344 -3722 metaprl/theories/czf/czf_itt_group_bvd.prla
Added metaprl/theories/czf/czf_itt_group_power.ml
Properties metaprl/theories/czf/czf_itt_group_power.ml
Added metaprl/theories/czf/czf_itt_group_power.mli
Properties metaprl/theories/czf/czf_itt_group_power.mli
Added metaprl/theories/czf/czf_itt_group_power.prla
Properties metaprl/theories/czf/czf_itt_group_power.prla
+13 -24 metaprl/theories/czf/czf_itt_hom.ml
+1 -1 metaprl/theories/czf/czf_itt_hom.mli
+11946 -13211 metaprl/theories/czf/czf_itt_hom.prla
+1 -11 metaprl/theories/czf/czf_itt_iso.ml
+1 -1 metaprl/theories/czf/czf_itt_iso.mli
+4023 -4860 metaprl/theories/czf/czf_itt_iso.prla
+23 -23 metaprl/theories/czf/czf_itt_ker.ml
+3 -3 metaprl/theories/czf/czf_itt_ker.mli
+12700 -15057 metaprl/theories/czf/czf_itt_ker.prla
+37 -66 metaprl/theories/czf/czf_itt_kleingroup.ml
+2 -2 metaprl/theories/czf/czf_itt_kleingroup.mli
+9198 -13326 metaprl/theories/czf/czf_itt_kleingroup.prla
+2 -3 metaprl/theories/czf/czf_itt_normal_subgroup.ml
+0 -1 metaprl/theories/czf/czf_itt_normal_subgroup.mli
+4166 -4173 metaprl/theories/czf/czf_itt_normal_subgroup.prla
+29 -32 metaprl/theories/czf/czf_itt_subgroup.ml
+1 -2 metaprl/theories/czf/czf_itt_subgroup.mli
+5623 -7492 metaprl/theories/czf/czf_itt_subgroup.prla