equal
deleted
inserted
replaced
1 (* Title : PReal.thy |
1 (* Title : PReal.thy |
|
2 ID : $Id$ |
2 Author : Jacques D. Fleuriot |
3 Author : Jacques D. Fleuriot |
3 Copyright : 1998 University of Cambridge |
4 Copyright : 1998 University of Cambridge |
4 Description : The positive reals as Dedekind sections of positive |
5 Description : The positive reals as Dedekind sections of positive |
5 rationals. Fundamentals of Abstract Analysis [Gleason- p. 121] |
6 rationals. Fundamentals of Abstract Analysis [Gleason- p. 121] |
6 provides some of the definitions. |
7 provides some of the definitions. |