# HG changeset patch
# User mehta
# Date 1084784536 -7200
# Node ID 3fc3c7b7e99d80107276d08de3442f614b24f88d
# Parent  0d7850e27fed4b30d7d2743b0e127dd13b85f045
lemma disjoint_int_union removed - too special

diff -r 0d7850e27fed -r 3fc3c7b7e99d src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri May 14 19:29:22 2004 +0200
+++ b/src/HOL/Set.thy	Mon May 17 11:02:16 2004 +0200
@@ -1107,10 +1107,6 @@
  "({} = A \<inter> insert b B) = (b \<notin> A \<and> {} = A \<inter> B)"
 by auto
 
-lemma disjoint_int_union[simp]:
-  "({} = A \<inter> (B \<union> C)) = ({} = A \<inter> B \<and> {} = A \<inter> C)"
-by blast
-
 text {* \medskip @{text image}. *}
 
 lemma image_empty [simp]: "f`{} = {}"
@@ -1288,7 +1284,6 @@
 
 lemma Un_empty [iff]: "(A \<union> B = {}) = (A = {} & B = {})"
   by blast
-
 lemma Un_subset_iff: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
   by blast