changeset 44890 | 22f665a2e91c |
parent 44142 | 8e27e0177518 |
child 47443 | aeff49a3369b |
--- a/src/HOL/Library/Set_Algebras.thy Sun Sep 11 22:56:05 2011 +0200 +++ b/src/HOL/Library/Set_Algebras.thy Mon Sep 12 07:55:43 2011 +0200 @@ -356,7 +356,7 @@ lemma set_plus_image: fixes S T :: "'n::semigroup_add set" shows "S \<oplus> T = (\<lambda>(x, y). x + y) ` (S \<times> T)" - unfolding set_plus_def by (fastsimp simp: image_iff) + unfolding set_plus_def by (fastforce simp: image_iff) lemma set_setsum_alt: assumes fin: "finite I"