src/HOL/Algebra/AbelCoset.thy
changeset 23383 5460951833fa
parent 23350 50c5b0912a0c
child 23463 9953ff53cc64
     1.1 --- a/src/HOL/Algebra/AbelCoset.thy	Thu Jun 14 09:54:14 2007 +0200
     1.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Thu Jun 14 10:38:48 2007 +0200
     1.3 @@ -712,7 +712,7 @@
     1.4        and repr:  "H +> x = H +> y"
     1.5    shows "y \<in> H +> x"
     1.6  by (rule group.repr_independenceD [OF a_group a_subgroup,
     1.7 -    folded a_r_coset_def, simplified monoid_record_simps])
     1.8 +    folded a_r_coset_def, simplified monoid_record_simps]) (rule ycarr, rule repr)
     1.9  
    1.10  
    1.11  subsection {* Lemmas for the Set of Right Cosets *}
    1.12 @@ -731,7 +731,7 @@
    1.13        and Bcarr: "B \<subseteq> carrier G"
    1.14    shows "A <+> B \<subseteq> carrier G"
    1.15  by (rule monoid.set_mult_closed [OF a_monoid,
    1.16 -    folded set_add_def, simplified monoid_record_simps])
    1.17 +    folded set_add_def, simplified monoid_record_simps]) (rule Acarr, rule Bcarr)
    1.18  
    1.19  lemma (in abelian_group) add_additive_subgroups:
    1.20    assumes subH: "additive_subgroup H G"