# HG changeset patch
# User haftmann
# Date 1311312809 -7200
# Node ID b1b436f7507055193e872ac39e755e493b9e34d5
# Parent  e6928fc2332a5b7bd27e629b7ac9220f5d0b9473
dropped errorneous hint

diff -r e6928fc2332a -r b1b436f75070 src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Thu Jul 21 22:47:13 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy	Fri Jul 22 07:33:29 2011 +0200
@@ -941,7 +941,7 @@
 lemma UN_eq: "(\<Union>x\<in>A. B x) = \<Union>({Y. \<exists>x\<in>A. Y = B x})"
   by (fact SUP_eq)
 
-lemma image_Union: "f ` \<Union>S = (\<Union>x\<in>S. f ` x)" -- "FIXME generalize"
+lemma image_Union: "f ` \<Union>S = (\<Union>x\<in>S. f ` x)"
   by blast
 
 lemma UNION_empty_conv[simp]: