diff -r 6b7c64ab8bd2 -r 75e1aa7a450e src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy Thu May 28 10:18:46 2015 +0200
+++ b/src/HOL/Complete_Lattices.thy Thu May 28 14:33:35 2015 +0100
@@ -1204,6 +1204,9 @@
"\(B ` A) = (\x\A. B x)"
by (fact Sup_image_eq)
+lemma Union_SetCompr_eq: "\ {f x| x. P x} = {a. \x. P x \ a \ f x}"
+ by blast
+
lemma UN_iff [simp]: "b \ (\x\A. B x) \ (\x\A. b \ B x)"
using Union_iff [of _ "B ` A"] by simp