1.1 --- a/src/HOL/Deriv.thy	Mon Jul 19 20:23:52 2010 +0200
     1.2 +++ b/src/HOL/Deriv.thy	Tue Jul 20 06:35:29 2010 +0200
     1.3 @@ -1255,8 +1255,9 @@
     1.4    assume "~ f a \<le> f b"
     1.5    assume "a = b"
     1.6    with prems show False by auto
     1.7 -  next assume "~ f a \<le> f b"
     1.8 -  assume "a ~= b"
     1.9 +next
    1.10 +  assume A: "~ f a \<le> f b"
    1.11 +  assume B: "a ~= b"
    1.12    with assms have "EX l z. a < z & z < b & DERIV f z :> l
    1.13        & f b - f a = (b - a) * l"
    1.14      apply -
    1.15 @@ -1266,11 +1267,11 @@
    1.16       apply (metis differentiableI less_le)
    1.17      done
    1.18    then obtain l z where "a < z" and "z < b" and "DERIV f z :> l"
    1.19 -      and "f b - f a = (b - a) * l"
    1.20 +      and C: "f b - f a = (b - a) * l"
    1.21      by auto
    1.22 -  from prems have "~(l >= 0)"
    1.23 -    by (metis diff_self diff_eq_diff_less_eq le_iff_diff_le_0 order_antisym linear
    1.24 -              split_mult_pos_le)
    1.25 +  with A have "a < b" "f b < f a" by auto
    1.26 +  with C have "\<not> l \<ge> 0" by (auto simp add: not_le algebra_simps)
    1.27 +    (metis A add_le_cancel_right assms(1) less_eq_real_def mult_right_mono real_add_left_mono real_le_linear real_le_refl)
    1.28    with prems show False
    1.29      by (metis DERIV_unique order_less_imp_le)
    1.30  qed