--- 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