src/HOL/Set.thy
changeset 13103 66659a4b16f6
parent 12937 0c4fd7529467
child 13113 5eb9be7b72a5
     1.1 --- a/src/HOL/Set.thy	Sat May 04 15:47:21 2002 +0200
     1.2 +++ b/src/HOL/Set.thy	Mon May 06 09:42:20 2002 +0200
     1.3 @@ -1049,6 +1049,13 @@
     1.4  lemma UN_insert_distrib: "u \<in> A ==> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)"
     1.5    by blast
     1.6  
     1.7 +lemma insert_disjoint[simp]:
     1.8 + "(insert a A \<inter> B = {}) = (a \<notin> B \<and> A \<inter> B = {})"
     1.9 +by blast
    1.10 +
    1.11 +lemma disjoint_insert[simp]:
    1.12 + "(B \<inter> insert a A = {}) = (a \<notin> B \<and> B \<inter> A = {})"
    1.13 +by blast
    1.14  
    1.15  text {* \medskip @{text image}. *}
    1.16