changeset 36794 | f736a853864f |
parent 36793 | 27da0a27b76f |
child 37388 | 793618618f78 |
--- a/src/HOL/ex/Dedekind_Real.thy Mon May 10 11:30:05 2010 -0700 +++ b/src/HOL/ex/Dedekind_Real.thy Mon May 10 11:47:56 2010 -0700 @@ -1,5 +1,6 @@ (* Title: HOL/ex/Dedekind_Real.thy Author: Jacques D. Fleuriot, University of Cambridge + Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4 The positive reals as Dedekind sections of positive rationals. Fundamentals of Abstract Analysis [Gleason- p. 121]