--- a/src/HOL/Set.thy Thu Jun 04 15:00:44 2009 +0200
+++ b/src/HOL/Set.thy Thu Jun 04 19:44:06 2009 +0200
@@ -1344,13 +1344,16 @@
by auto
lemma image_image: "f ` (g ` A) = (\<lambda>x. f (g x)) ` A"
- by blast
+by blast
lemma insert_image [simp]: "x \<in> A ==> insert (f x) (f`A) = f`A"
- by blast
+by blast
lemma image_is_empty [iff]: "(f`A = {}) = (A = {})"
- by blast
+by blast
+
+lemma empty_is_image[iff]: "({} = f ` A) = (A = {})"
+by blast
lemma image_Collect [noatp]: "f ` {x. P x} = {f x | x. P x}"