equal
deleted
inserted
replaced
301 proof for part (1); this part is left to the reader''. But this is precisely |
301 proof for part (1); this part is left to the reader''. But this is precisely |
302 the part that requires the intermediate value theorem and thus is not at all |
302 the part that requires the intermediate value theorem and thus is not at all |
303 similar to the other cases (which are automatic in Isabelle). We conclude |
303 similar to the other cases (which are automatic in Isabelle). We conclude |
304 that the authors are at least cavalier about this point and may even have |
304 that the authors are at least cavalier about this point and may even have |
305 overlooked the slight difficulty lurking in the omitted cases. This is not |
305 overlooked the slight difficulty lurking in the omitted cases. This is not |
306 atypical for pencil-and-paper proofs, once analysed in detail. *} |
306 atypical for pen-and-paper proofs, once analysed in detail. *} |
307 |
307 |
308 (*<*)end(*>*) |
308 (*<*)end(*>*) |