1.1 --- a/src/HOL/Algebra/Group.thy	Sun Oct 18 00:10:20 2009 +0200
     1.2 +++ b/src/HOL/Algebra/Group.thy	Sun Oct 18 12:07:56 2009 +0200
     1.3 @@ -553,11 +553,11 @@
     1.4  by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
     1.5  
     1.6  lemma (in group) iso_sym:
     1.7 -     "h \<in> G \<cong> H \<Longrightarrow> Inv (carrier G) h \<in> H \<cong> G"
     1.8 -apply (simp add: iso_def bij_betw_Inv) 
     1.9 -apply (subgoal_tac "Inv (carrier G) h \<in> carrier H \<rightarrow> carrier G") 
    1.10 - prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_Inv]) 
    1.11 -apply (simp add: hom_def bij_betw_def Inv_f_eq f_Inv_f Pi_def)
    1.12 +     "h \<in> G \<cong> H \<Longrightarrow> inv_onto (carrier G) h \<in> H \<cong> G"
    1.13 +apply (simp add: iso_def bij_betw_inv_onto) 
    1.14 +apply (subgoal_tac "inv_onto (carrier G) h \<in> carrier H \<rightarrow> carrier G") 
    1.15 + prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_inv_onto]) 
    1.16 +apply (simp add: hom_def bij_betw_def inv_onto_f_eq f_inv_onto_f Pi_def)
    1.17  done
    1.18  
    1.19  lemma (in group) iso_trans: