src/HOL/ex/Locales.thy
changeset 19931 fb32b43e7f80
parent 17388 495c799df31d
     1.1 --- a/src/HOL/ex/Locales.thy	Tue Jun 20 14:51:59 2006 +0200
     1.2 +++ b/src/HOL/ex/Locales.thy	Tue Jun 20 15:53:44 2006 +0200
     1.3 @@ -481,7 +481,7 @@
     1.4  	semigroup_product_def semigroup.defs)
     1.5      moreover
     1.6      have "semigroup ?G'" and "semigroup ?H'"
     1.7 -      using prems by (simp_all add: semigroup_def semigroup.defs)
     1.8 +      using prems by (simp_all add: semigroup_def semigroup.defs G.assoc H.assoc)
     1.9      then have "semigroup (semigroup_product ?G' ?H')" ..
    1.10      ultimately show ?thesis by (simp add: I_def semigroup_def)
    1.11    qed