src/HOL/Hyperreal/Lim.thy

--- a/src/HOL/Hyperreal/Lim.thy	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Hyperreal/Lim.thy	Sat Oct 06 00:02:46 2001 +0200
@@ -71,8 +71,8 @@
   "Bolzano_bisect P a b 0 = (a,b)"
   "Bolzano_bisect P a b (Suc n) =
       (let (x,y) = Bolzano_bisect P a b n
-       in if P(x, (x+y)/# 2) then ((x+y)/# 2, y)
-                            else (x, (x+y)/# 2) )"
+       in if P(x, (x+y)/2) then ((x+y)/2, y)
+                            else (x, (x+y)/2) )"
   
 
 end