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