1.1 --- a/src/HOL/Complete_Lattice.thy	Mon Jul 18 21:49:39 2011 +0200
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Mon Jul 18 21:52:34 2011 +0200
     1.3 @@ -730,36 +730,36 @@
     1.4    by auto
     1.5  
     1.6  lemma Union_upper: "B \<in> A \<Longrightarrow> B \<subseteq> \<Union>A"
     1.7 -  by (iprover intro: subsetI UnionI)
     1.8 +  by (fact Sup_upper)
     1.9  
    1.10  lemma Union_least: "(\<And>X. X \<in> A \<Longrightarrow> X \<subseteq> C) \<Longrightarrow> \<Union>A \<subseteq> C"
    1.11 -  by (iprover intro: subsetI elim: UnionE dest: subsetD)
    1.12 +  by (fact Sup_least)
    1.13  
    1.14  lemma Un_eq_Union: "A \<union> B = \<Union>{A, B}"
    1.15    by blast
    1.16  
    1.17  lemma Union_empty [simp]: "\<Union>{} = {}"
    1.18 -  by blast
    1.19 +  by (fact Sup_empty)
    1.20  
    1.21  lemma Union_UNIV [simp]: "\<Union>UNIV = UNIV"
    1.22 -  by blast
    1.23 +  by (fact Sup_UNIV)
    1.24  
    1.25  lemma Union_insert [simp]: "\<Union>insert a B = a \<union> \<Union>B"
    1.26 -  by blast
    1.27 +  by (fact Sup_insert)
    1.28  
    1.29  lemma Union_Un_distrib [simp]: "\<Union>(A \<union> B) = \<Union>A \<union> \<Union>B"
    1.30 -  by blast
    1.31 +  by (fact Sup_union_distrib)
    1.32  
    1.33  lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>A \<inter> \<Union>B"
    1.34 -  by blast
    1.35 +  by (fact Sup_inter_less_eq)
    1.36  
    1.37  lemma Union_empty_conv [simp,no_atp]: "(\<Union>A = {}) \<longleftrightarrow> (\<forall>x\<in>A. x = {})"
    1.38 -  by blast
    1.39 +  by (fact Sup_bot_conv)
    1.40  
    1.41  lemma empty_Union_conv [simp,no_atp]: "({} = \<Union>A) \<longleftrightarrow> (\<forall>x\<in>A. x = {})"
    1.42 -  by blast
    1.43 +  by (fact Sup_bot_conv)
    1.44  
    1.45 -lemma Union_disjoint: "(\<Union>C \<inter> A = {}) \<longleftrightarrow> (\<forall>B\<in>C. B \<inter> A = {})"
    1.46 +lemma Union_disjoint: "(\<Union>C \<inter> A = {}) \<longleftrightarrow> (\<forall>B\<in>C. B \<inter> A = {})" -- "FIXME generalize"
    1.47    by blast
    1.48  
    1.49  lemma subset_Pow_Union: "A \<subseteq> Pow (\<Union>A)"
    1.50 @@ -769,7 +769,7 @@
    1.51    by blast
    1.52  
    1.53  lemma Union_mono: "A \<subseteq> B \<Longrightarrow> \<Union>A \<subseteq> \<Union>B"
    1.54 -  by blast
    1.55 +  by (fact Sup_subset_mono)
    1.56  
    1.57  
    1.58  subsection {* Unions of families *}