src/HOL/Algebra/AbelCoset.thy
changeset 23463 9953ff53cc64
parent 23383 5460951833fa
child 26203 9625f3579b48
     1.1 --- a/src/HOL/Algebra/AbelCoset.thy	Thu Jun 21 17:28:50 2007 +0200
     1.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Thu Jun 21 17:28:53 2007 +0200
     1.3 @@ -700,12 +700,14 @@
     1.4  qed
     1.5  
     1.6  lemma (in abelian_subgroup) a_repr_independence':
     1.7 -  assumes "y \<in> H +> x"
     1.8 -      and "x \<in> carrier G"
     1.9 +  assumes y: "y \<in> H +> x"
    1.10 +      and xcarr: "x \<in> carrier G"
    1.11    shows "H +> x = H +> y"
    1.12 -apply (rule a_repr_independence, assumption+)
    1.13 -apply (rule a_subgroup)
    1.14 -done
    1.15 +  apply (rule a_repr_independence)
    1.16 +    apply (rule y)
    1.17 +   apply (rule xcarr)
    1.18 +  apply (rule a_subgroup)
    1.19 +  done
    1.20  
    1.21  lemma (in abelian_subgroup) a_repr_independenceD:
    1.22    assumes ycarr: "y \<in> carrier G"