Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-05-19 00:21:32 -0700 (Sun, 19 May 2002)
Revision: 3676
Log message:

      The former definition for group builder was not consistent. Now group_bvd{h; g; s} also requires that subset{s; car{g}}. From it, it can be proven that id{h} = id{g} and inv{h; a} = inv{g; a} for all a in car{h}.
      Reproved all related rules and updated related comments.
      

Changes  Path
+31 -6 metaprl/theories/czf/czf_itt_group_bvd.ml
+4 -2 metaprl/theories/czf/czf_itt_group_bvd.mli
+1839 -687 metaprl/theories/czf/czf_itt_group_bvd.prla
+8 -6 metaprl/theories/czf/czf_itt_hom.ml
+888 -989 metaprl/theories/czf/czf_itt_hom.prla
+8 -4 metaprl/theories/czf/czf_itt_ker.ml
+1 -2 metaprl/theories/czf/czf_itt_ker.mli
+1372 -1279 metaprl/theories/czf/czf_itt_ker.prla
+6 -4 metaprl/theories/czf/czf_itt_subgroup.ml
+0 -1 metaprl/theories/czf/czf_itt_subgroup.mli
+2594 -2598 metaprl/theories/czf/czf_itt_subgroup.prla