src/HOL/Lim.thy
changeset 32642 026e7c6a6d08
parent 32436 10cd49e0c067
child 32650 34bfa2492298
     1.1 --- a/src/HOL/Lim.thy	Mon Sep 21 16:11:36 2009 +0200
     1.2 +++ b/src/HOL/Lim.thy	Tue Sep 22 15:36:55 2009 +0200
     1.3 @@ -544,7 +544,7 @@
     1.4      case True thus ?thesis using `0 < s` by auto
     1.5    next
     1.6      case False hence "s / 2 \<ge> (x - b) / 2" by auto
     1.7 -    hence "?x = (x + b) / 2" by(simp add:field_simps)
     1.8 +    hence "?x = (x + b) / 2" by (simp add: field_simps min_max.inf_absorb2)
     1.9      thus ?thesis using `b < x` by auto
    1.10    qed
    1.11    hence "0 \<le> f ?x" using all_le `?x < x` by auto