--- a/src/HOL/Algebra/Group.thy Wed Oct 21 17:34:35 2009 +0200
+++ b/src/HOL/Algebra/Group.thy Thu Oct 22 09:27:48 2009 +0200
@@ -553,11 +553,11 @@
by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
lemma (in group) iso_sym:
- "h \<in> G \<cong> H \<Longrightarrow> inv_onto (carrier G) h \<in> H \<cong> G"
-apply (simp add: iso_def bij_betw_inv_onto)
-apply (subgoal_tac "inv_onto (carrier G) h \<in> carrier H \<rightarrow> carrier G")
- prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_inv_onto])
-apply (simp add: hom_def bij_betw_def inv_onto_f_eq f_inv_onto_f Pi_def)
+ "h \<in> G \<cong> H \<Longrightarrow> inv_into (carrier G) h \<in> H \<cong> G"
+apply (simp add: iso_def bij_betw_inv_into)
+apply (subgoal_tac "inv_into (carrier G) h \<in> carrier H \<rightarrow> carrier G")
+ prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_inv_into])
+apply (simp add: hom_def bij_betw_def inv_into_f_eq f_inv_into_f Pi_def)
done
lemma (in group) iso_trans: