--- 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