src/HOL/Real/RealDef.thy
changeset 7127 48e235179ffb
parent 7077 60b098bb8b8a
child 7219 4e3f386c2e37
equal deleted inserted replaced
7126:fdb397af4cab 7127:48e235179ffb
    31             preal_of_prat(prat_of_pnat 1p),preal_of_prat(prat_of_pnat 1p))})"
    31             preal_of_prat(prat_of_pnat 1p),preal_of_prat(prat_of_pnat 1p))})"
    32 
    32 
    33   real_minus_def
    33   real_minus_def
    34     "- R ==  Abs_real(UN (x,y):Rep_real(R). realrel^^{(y,x)})"
    34     "- R ==  Abs_real(UN (x,y):Rep_real(R). realrel^^{(y,x)})"
    35 
    35 
    36   real_diff_def "x - y == x + -(y::real)"
    36   real_diff_def "x - y == x + (- y :: real)"
    37 
    37 
    38 constdefs
    38 constdefs
    39 
    39 
    40   real_of_preal :: preal => real            
    40   real_of_preal :: preal => real            
    41   "real_of_preal m     ==
    41   "real_of_preal m     ==
    47 
    47 
    48   real_of_posnat :: nat => real             
    48   real_of_posnat :: nat => real             
    49   "real_of_posnat n == real_of_preal(preal_of_prat(prat_of_pnat(pnat_of_nat n)))"
    49   "real_of_posnat n == real_of_preal(preal_of_prat(prat_of_pnat(pnat_of_nat n)))"
    50 
    50 
    51   real_of_nat :: nat => real          
    51   real_of_nat :: nat => real          
    52   "real_of_nat n    == real_of_posnat n + -1r"
    52   "real_of_nat n    == real_of_posnat n + (-1r)"
    53 
    53 
    54 defs
    54 defs
    55 
    55 
    56   real_add_def  
    56   real_add_def  
    57   "P + Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q).
    57   "P + Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q).