src/HOL/Lim.thy

--- a/src/HOL/Lim.thy	Mon Sep 21 16:11:36 2009 +0200
+++ b/src/HOL/Lim.thy	Tue Sep 22 15:36:55 2009 +0200
@@ -544,7 +544,7 @@
     case True thus ?thesis using `0 < s` by auto
   next
     case False hence "s / 2 \<ge> (x - b) / 2" by auto
-    hence "?x = (x + b) / 2" by(simp add:field_simps)
+    hence "?x = (x + b) / 2" by (simp add: field_simps min_max.inf_absorb2)
     thus ?thesis using `b < x` by auto
   qed
   hence "0 \<le> f ?x" using all_le `?x < x` by auto