# HG changeset patch
# User huffman
# Date 1269797642 25200
# Node ID 095b1022e2ae8a54781b1125548322ad8e06abfa
# Parent  f4f34350024925abf2672fca574066317605dbae
cleaned up some proofs

diff -r f4f343500249 -r 095b1022e2ae src/HOL/SupInf.thy
--- a/src/HOL/SupInf.thy	Sun Mar 28 17:43:09 2010 +0200
+++ b/src/HOL/SupInf.thy	Sun Mar 28 10:34:02 2010 -0700
@@ -106,10 +106,10 @@
 proof (cases "Sup X \<le> a")
   case True
   thus ?thesis
-    apply (simp add: max_def) 
+    apply (simp add: max_def)
     apply (rule Sup_eq_maximum)
-    apply (metis insertCI)
-    apply (metis Sup_upper insertE le_iff_sup real_le_linear real_le_trans sup_absorb1 z)     
+    apply (rule insertI1)
+    apply (metis Sup_upper [OF _ z] insertE real_le_linear real_le_trans)
     done
 next
   case False
@@ -177,7 +177,7 @@
   fixes S :: "real set"
   assumes fS: "finite S" and Se: "S \<noteq> {}"
   shows "a \<ge> Sup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> x)"
-by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS le_iff_sup real_le_trans) 
+by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS real_le_trans)
 
 lemma Sup_finite_gt_iff: 
   fixes S :: "real set"
@@ -331,8 +331,8 @@
   have "Inf (insert a X) \<le> Inf X"
     apply (rule Inf_greatest)
     apply (metis empty_psubset_nonempty psubset_eq x)
-    apply (rule Inf_lower_EX) 
-    apply (blast intro: elim:) 
+    apply (rule Inf_lower_EX)
+    apply (erule insertI2)
     apply (metis insert_iff real_le_linear real_le_refl real_le_trans z)
     done
   moreover