| changeset 22710 | f44439cdce77 |
| parent 22483 | 86064f2f2188 |
| child 23285 | c95a4f6b3881 |
--- a/src/HOL/Real/PReal.thy Sun Apr 15 23:25:50 2007 +0200 +++ b/src/HOL/Real/PReal.thy Sun Apr 15 23:25:52 2007 +0200 @@ -932,7 +932,7 @@ subsection{*Subtraction for Positive Reals*} -text{*Gleason prop. 9-3.5(iv), page 123: proving @{term "A < B ==> \<exists>D. A + D = +text{*Gleason prop. 9-3.5(iv), page 123: proving @{prop "A < B ==> \<exists>D. A + D = B"}. We define the claimed @{term D} and show that it is a positive real*} text{*Part 1 of Dedekind sections definition*}