equal
deleted
inserted
replaced
4 Copyright : 1998 University of Cambridge |
4 Copyright : 1998 University of Cambridge |
5 Description : The positive reals as Dedekind sections of positive |
5 Description : The positive reals as Dedekind sections of positive |
6 rationals. Fundamentals of Abstract Analysis [Gleason- p. 121] |
6 rationals. Fundamentals of Abstract Analysis [Gleason- p. 121] |
7 provides some of the definitions. |
7 provides some of the definitions. |
8 *) |
8 *) |
|
9 |
|
10 header {* Positive real numbers *} |
9 |
11 |
10 theory PReal |
12 theory PReal |
11 imports Rational |
13 imports Rational |
12 begin |
14 begin |
13 |
15 |