--- a/src/HOL/Set.thy Mon Aug 02 16:06:13 2004 +0200
+++ b/src/HOL/Set.thy Tue Aug 03 13:48:00 2004 +0200
@@ -1275,7 +1275,7 @@
lemma Int_UNIV [simp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
by blast
-lemma Int_subset_iff: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
+lemma Int_subset_iff [simp]: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
by blast
lemma Int_Collect: "(x \<in> A \<inter> {x. P x}) = (x \<in> A & P x)"
@@ -1352,7 +1352,8 @@
lemma Un_empty [iff]: "(A \<union> B = {}) = (A = {} & B = {})"
by blast
-lemma Un_subset_iff: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
+
+lemma Un_subset_iff [simp]: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
by blast
lemma Un_Diff_Int: "(A - B) \<union> (A \<inter> B) = A"
@@ -1473,7 +1474,7 @@
by blast
lemma UN_absorb: "k \<in> I ==> A k \<union> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. A i)"
- by blast
+ by auto
lemma INT_empty [simp]: "(\<Inter>x\<in>{}. B x) = UNIV"
by blast