src/HOL/Set.thy
 changeset 15102 04b0e943fcc9 parent 14981 e73f8140af78 child 15120 f0359f75682e
```     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
```