changeset 11704 | 3c50a2cd6f00 |
parent 11701 | 3d51fbf81c17 |
child 12018 | ec054019c910 |
--- 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