| changeset 11704 | 3c50a2cd6f00 |
| parent 11701 | 3d51fbf81c17 |
| child 12018 | ec054019c910 |
| 11703:6e5de8d4290a | 11704:3c50a2cd6f00 |
|---|---|
69 |
69 |
70 primrec |
70 primrec |
71 "Bolzano_bisect P a b 0 = (a,b)" |
71 "Bolzano_bisect P a b 0 = (a,b)" |
72 "Bolzano_bisect P a b (Suc n) = |
72 "Bolzano_bisect P a b (Suc n) = |
73 (let (x,y) = Bolzano_bisect P a b n |
73 (let (x,y) = Bolzano_bisect P a b n |
74 in if P(x, (x+y)/# 2) then ((x+y)/# 2, y) |
74 in if P(x, (x+y)/2) then ((x+y)/2, y) |
75 else (x, (x+y)/# 2) )" |
75 else (x, (x+y)/2) )" |
76 |
76 |
77 |
77 |
78 end |
78 end |
79 |
79 |