--- a/src/HOL/Set.thy Mon Sep 02 17:14:51 2013 +0200
+++ b/src/HOL/Set.thy Mon Sep 02 17:57:56 2013 +0200
@@ -883,6 +883,13 @@
lemma doubleton_eq_iff: "({a,b} = {c,d}) = (a=c & b=d | a=d & b=c)"
by (blast elim: equalityE)
+lemma Un_singleton_iff:
+ "(A \<union> B = {x}) = (A = {} \<and> B = {x} \<or> A = {x} \<and> B = {} \<or> A = {x} \<and> B = {x})"
+by auto
+
+lemma singleton_Un_iff:
+ "({x} = A \<union> B) = (A = {} \<and> B = {x} \<or> A = {x} \<and> B = {} \<or> A = {x} \<and> B = {x})"
+by auto
subsubsection {* Image of a set under a function *}