--- a/src/HOL/Algebra/Bij.thy Wed May 19 11:29:47 2004 +0200
+++ b/src/HOL/Algebra/Bij.thy Wed May 19 11:30:18 2004 +0200
@@ -133,7 +133,8 @@
apply (blast intro: dest: id_in_auto)
apply (simp del: restrict_apply
add: inv_BijGroup auto_def restrict_Inv_Bij restrict_Inv_hom)
-apply (simp add: BijGroup_def auto_def Bij_imp_funcset compose_hom compose_Bij)
+apply (auto simp add: BijGroup_def auto_def Bij_imp_funcset group.hom_compose
+ compose_Bij)
done
theorem AutoGroup: "group G ==> group (AutoGroup G)"