src/HOL/Algebra/Bij.thy
changeset 14761 28b5eb4a867f
parent 14706 71590b7733b7
child 14853 8d710bece29f
     1.1 --- a/src/HOL/Algebra/Bij.thy	Wed May 19 11:29:47 2004 +0200
     1.2 +++ b/src/HOL/Algebra/Bij.thy	Wed May 19 11:30:18 2004 +0200
     1.3 @@ -133,7 +133,8 @@
     1.4    apply (blast intro: dest: id_in_auto)
     1.5   apply (simp del: restrict_apply
     1.6               add: inv_BijGroup auto_def restrict_Inv_Bij restrict_Inv_hom)
     1.7 -apply (simp add: BijGroup_def auto_def Bij_imp_funcset compose_hom compose_Bij)
     1.8 +apply (auto simp add: BijGroup_def auto_def Bij_imp_funcset group.hom_compose
     1.9 +                      compose_Bij)
    1.10  done
    1.11  
    1.12  theorem AutoGroup: "group G ==> group (AutoGroup G)"