# HG changeset patch
# User haftmann
# Date 1311018754 -7200
# Node ID 3ab6c30d256dac49c5fe6769b55cbefc98d9ab2c
# Parent  7162691e740bf34b2ac4902d7da06d99006c0f59
proof tuning

diff -r 7162691e740b -r 3ab6c30d256d src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Mon Jul 18 21:49:39 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy	Mon Jul 18 21:52:34 2011 +0200
@@ -730,36 +730,36 @@
   by auto
 
 lemma Union_upper: "B \<in> A \<Longrightarrow> B \<subseteq> \<Union>A"
-  by (iprover intro: subsetI UnionI)
+  by (fact Sup_upper)
 
 lemma Union_least: "(\<And>X. X \<in> A \<Longrightarrow> X \<subseteq> C) \<Longrightarrow> \<Union>A \<subseteq> C"
-  by (iprover intro: subsetI elim: UnionE dest: subsetD)
+  by (fact Sup_least)
 
 lemma Un_eq_Union: "A \<union> B = \<Union>{A, B}"
   by blast
 
 lemma Union_empty [simp]: "\<Union>{} = {}"
-  by blast
+  by (fact Sup_empty)
 
 lemma Union_UNIV [simp]: "\<Union>UNIV = UNIV"
-  by blast
+  by (fact Sup_UNIV)
 
 lemma Union_insert [simp]: "\<Union>insert a B = a \<union> \<Union>B"
-  by blast
+  by (fact Sup_insert)
 
 lemma Union_Un_distrib [simp]: "\<Union>(A \<union> B) = \<Union>A \<union> \<Union>B"
-  by blast
+  by (fact Sup_union_distrib)
 
 lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>A \<inter> \<Union>B"
-  by blast
+  by (fact Sup_inter_less_eq)
 
 lemma Union_empty_conv [simp,no_atp]: "(\<Union>A = {}) \<longleftrightarrow> (\<forall>x\<in>A. x = {})"
-  by blast
+  by (fact Sup_bot_conv)
 
 lemma empty_Union_conv [simp,no_atp]: "({} = \<Union>A) \<longleftrightarrow> (\<forall>x\<in>A. x = {})"
-  by blast
+  by (fact Sup_bot_conv)
 
-lemma Union_disjoint: "(\<Union>C \<inter> A = {}) \<longleftrightarrow> (\<forall>B\<in>C. B \<inter> A = {})"
+lemma Union_disjoint: "(\<Union>C \<inter> A = {}) \<longleftrightarrow> (\<forall>B\<in>C. B \<inter> A = {})" -- "FIXME generalize"
   by blast
 
 lemma subset_Pow_Union: "A \<subseteq> Pow (\<Union>A)"
@@ -769,7 +769,7 @@
   by blast
 
 lemma Union_mono: "A \<subseteq> B \<Longrightarrow> \<Union>A \<subseteq> \<Union>B"
-  by blast
+  by (fact Sup_subset_mono)
 
 
 subsection {* Unions of families *}