# HG changeset patch
# User nipkow
# Date 1378134779 -7200
# Node ID a4fff0c0599c71b5e29ee265e304945a554e6cd5
# Parent  7ffc4a746a73791e4f6993be0ca0e764d5ac4e98
added lemmas

diff -r 7ffc4a746a73 -r a4fff0c0599c src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Sep 02 15:13:00 2013 +0200
+++ b/src/HOL/Set.thy	Mon Sep 02 17:12:59 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 *}