src/HOL/SupInf.thy
 changeset 36007 095b1022e2ae parent 35823 bd26885af9f4 child 36777 be5461582d0f
```     1.1 --- a/src/HOL/SupInf.thy	Sun Mar 28 17:43:09 2010 +0200
1.2 +++ b/src/HOL/SupInf.thy	Sun Mar 28 10:34:02 2010 -0700
1.3 @@ -106,10 +106,10 @@
1.4  proof (cases "Sup X \<le> a")
1.5    case True
1.6    thus ?thesis
1.7 -    apply (simp add: max_def)
1.8 +    apply (simp add: max_def)
1.9      apply (rule Sup_eq_maximum)
1.10 -    apply (metis insertCI)
1.11 -    apply (metis Sup_upper insertE le_iff_sup real_le_linear real_le_trans sup_absorb1 z)
1.12 +    apply (rule insertI1)
1.13 +    apply (metis Sup_upper [OF _ z] insertE real_le_linear real_le_trans)
1.14      done
1.15  next
1.16    case False
1.17 @@ -177,7 +177,7 @@
1.18    fixes S :: "real set"
1.19    assumes fS: "finite S" and Se: "S \<noteq> {}"
1.20    shows "a \<ge> Sup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> x)"
1.21 -by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS le_iff_sup real_le_trans)
1.22 +by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS real_le_trans)
1.23
1.24  lemma Sup_finite_gt_iff:
1.25    fixes S :: "real set"
1.26 @@ -331,8 +331,8 @@
1.27    have "Inf (insert a X) \<le> Inf X"
1.28      apply (rule Inf_greatest)
1.29      apply (metis empty_psubset_nonempty psubset_eq x)
1.30 -    apply (rule Inf_lower_EX)
1.31 -    apply (blast intro: elim:)
1.32 +    apply (rule Inf_lower_EX)
1.33 +    apply (erule insertI2)
1.34      apply (metis insert_iff real_le_linear real_le_refl real_le_trans z)
1.35      done
1.36    moreover
```