diff -r b6f8aae5f152 -r 66659a4b16f6 src/HOL/Set.thy
--- 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}. *}