src/HOL/Real/PReal.thy
changeset 17428 8a2de150b5f1
parent 16775 c1b87ef4a1c3
child 18215 a28879118978
equal deleted inserted replaced
17427:3c45d890d47c 17428:8a2de150b5f1
     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