--- a/src/HOL/Set.thy Sat May 04 15:47:21 2002 +0200
+++ b/src/HOL/Set.thy Mon May 06 09:42:20 2002 +0200
@@ -1049,6 +1049,13 @@
lemma UN_insert_distrib: "u \<in> A ==> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)"
by blast
+lemma insert_disjoint[simp]:
+ "(insert a A \<inter> B = {}) = (a \<notin> B \<and> A \<inter> B = {})"
+by blast
+
+lemma disjoint_insert[simp]:
+ "(B \<inter> insert a A = {}) = (a \<notin> B \<and> B \<inter> A = {})"
+by blast
text {* \medskip @{text image}. *}