1.1 --- a/src/HOL/Set.thy	Mon Aug 02 16:06:13 2004 +0200
     1.2 +++ b/src/HOL/Set.thy	Tue Aug 03 13:48:00 2004 +0200
     1.3 @@ -1275,7 +1275,7 @@
     1.4  lemma Int_UNIV [simp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
     1.5    by blast
     1.6  
     1.7 -lemma Int_subset_iff: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
     1.8 +lemma Int_subset_iff [simp]: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
     1.9    by blast
    1.10  
    1.11  lemma Int_Collect: "(x \<in> A \<inter> {x. P x}) = (x \<in> A & P x)"
    1.12 @@ -1352,7 +1352,8 @@
    1.13  
    1.14  lemma Un_empty [iff]: "(A \<union> B = {}) = (A = {} & B = {})"
    1.15    by blast
    1.16 -lemma Un_subset_iff: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
    1.17 +
    1.18 +lemma Un_subset_iff [simp]: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
    1.19    by blast
    1.20  
    1.21  lemma Un_Diff_Int: "(A - B) \<union> (A \<inter> B) = A"
    1.22 @@ -1473,7 +1474,7 @@
    1.23    by blast
    1.24  
    1.25  lemma UN_absorb: "k \<in> I ==> A k \<union> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. A i)"
    1.26 -  by blast
    1.27 +  by auto
    1.28  
    1.29  lemma INT_empty [simp]: "(\<Inter>x\<in>{}. B x) = UNIV"
    1.30    by blast