src/HOL/Algebra/Coset.thy
changeset 31727 2621a957d417
parent 30198 922f944f03b2
child 32960 69916a850301
     1.1 --- a/src/HOL/Algebra/Coset.thy	Fri Jun 19 20:22:46 2009 +0200
     1.2 +++ b/src/HOL/Algebra/Coset.thy	Fri Jun 19 22:49:12 2009 +0200
     1.3 @@ -934,8 +934,8 @@
     1.4  
     1.5  lemma (in group_hom) FactGroup_hom:
     1.6       "(\<lambda>X. contents (h`X)) \<in> hom (G Mod (kernel G H h)) H"
     1.7 -apply (simp add: hom_def FactGroup_contents_mem  normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)  
     1.8 -proof (simp add: hom_def funcsetI FactGroup_contents_mem, intro ballI) 
     1.9 +apply (simp add: hom_def FactGroup_contents_mem  normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
    1.10 +proof (intro ballI)
    1.11    fix X and X'
    1.12    assume X:  "X  \<in> carrier (G Mod kernel G H h)"
    1.13       and X': "X' \<in> carrier (G Mod kernel G H h)"
    1.14 @@ -952,7 +952,7 @@
    1.15               simp add: set_mult_def image_eq_UN 
    1.16                         subsetD [OF Xsub] subsetD [OF X'sub]) 
    1.17    thus "contents (h ` (X <#> X')) = contents (h ` X) \<otimes>\<^bsub>H\<^esub> contents (h ` X')"
    1.18 -    by (simp add: all image_eq_UN FactGroup_nonempty X X')  
    1.19 +    by (simp add: all image_eq_UN FactGroup_nonempty X X')
    1.20  qed
    1.21  
    1.22