1.1 --- a/src/HOL/Library/Set_Algebras.thy	Sun Sep 11 22:56:05 2011 +0200
     1.2 +++ b/src/HOL/Library/Set_Algebras.thy	Mon Sep 12 07:55:43 2011 +0200
     1.3 @@ -356,7 +356,7 @@
     1.4  
     1.5  lemma set_plus_image:
     1.6    fixes S T :: "'n::semigroup_add set" shows "S \<oplus> T = (\<lambda>(x, y). x + y) ` (S \<times> T)"
     1.7 -  unfolding set_plus_def by (fastsimp simp: image_iff)
     1.8 +  unfolding set_plus_def by (fastforce simp: image_iff)
     1.9  
    1.10  lemma set_setsum_alt:
    1.11    assumes fin: "finite I"