src/HOL/Algebra/AbelCoset.thy
changeset 26310 f8a7fac36e13
parent 26203 9625f3579b48
child 27192 005d4b953fdc
     1.1 --- a/src/HOL/Algebra/AbelCoset.thy	Mon Mar 17 20:51:23 2008 +0100
     1.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Mon Mar 17 22:34:23 2008 +0100
     1.3 @@ -413,7 +413,7 @@
     1.4  
     1.5  lemma (in abelian_subgroup) a_rcos_self:
     1.6    shows "x \<in> carrier G \<Longrightarrow> x \<in> H +> x"
     1.7 -by (rule group.rcos_self [OF a_group a_subgroup,
     1.8 +by (rule group.rcos_self [OF a_group _ a_subgroup,
     1.9      folded a_r_coset_def, simplified monoid_record_simps])
    1.10  
    1.11  lemma (in abelian_subgroup) a_rcosets_part_G: