lemma disjoint_int_union removed - too special
authormehta
Mon May 17 11:02:16 2004 +0200 (2004-05-17)
changeset 147523fc3c7b7e99d
parent 14751 0d7850e27fed
child 14753 f40b45db8cf0
lemma disjoint_int_union removed - too special
src/HOL/Set.thy
     1.1 --- a/src/HOL/Set.thy	Fri May 14 19:29:22 2004 +0200
     1.2 +++ b/src/HOL/Set.thy	Mon May 17 11:02:16 2004 +0200
     1.3 @@ -1107,10 +1107,6 @@
     1.4   "({} = A \<inter> insert b B) = (b \<notin> A \<and> {} = A \<inter> B)"
     1.5  by auto
     1.6  
     1.7 -lemma disjoint_int_union[simp]:
     1.8 -  "({} = A \<inter> (B \<union> C)) = ({} = A \<inter> B \<and> {} = A \<inter> C)"
     1.9 -by blast
    1.10 -
    1.11  text {* \medskip @{text image}. *}
    1.12  
    1.13  lemma image_empty [simp]: "f`{} = {}"
    1.14 @@ -1288,7 +1284,6 @@
    1.15  
    1.16  lemma Un_empty [iff]: "(A \<union> B = {}) = (A = {} & B = {})"
    1.17    by blast
    1.18 -
    1.19  lemma Un_subset_iff: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
    1.20    by blast
    1.21