# HG changeset patch
# User nipkow
# Date 1378137476 -7200
# Node ID 643e1151ed7ecd31f161031b9c81535f315ea25a
# Parent  f6629734dd2b5c36b697d2c608b869aafbb3f7d1# Parent  a4fff0c0599c71b5e29ee265e304945a554e6cd5
merged

diff -r f6629734dd2b -r 643e1151ed7e src/HOL/Set.thy
--- 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 *}