1.1 --- a/src/HOL/Real/RealDef.thy	Wed Dec 06 12:28:52 2000 +0100
     1.2 +++ b/src/HOL/Real/RealDef.thy	Wed Dec 06 12:34:12 2000 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4  
     1.5  
     1.6  instance
     1.7 -   real  :: {ord, zero, plus, times, minus}
     1.8 +   real  :: {ord, zero, plus, times, minus, inverse}
     1.9  
    1.10  consts 
    1.11  
    1.12 @@ -24,17 +24,24 @@
    1.13  defs
    1.14  
    1.15    real_zero_def  
    1.16 -     "0 == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p),
    1.17 +  "0 == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p),
    1.18                                  preal_of_prat(prat_of_pnat 1p))})"
    1.19    real_one_def   
    1.20 -     "1r == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p) + 
    1.21 +  "1r == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p) + 
    1.22              preal_of_prat(prat_of_pnat 1p),preal_of_prat(prat_of_pnat 1p))})"
    1.23  
    1.24    real_minus_def
    1.25 -    "- R ==  Abs_real(UN (x,y):Rep_real(R). realrel^^{(y,x)})"
    1.26 +  "- R ==  Abs_real(UN (x,y):Rep_real(R). realrel^^{(y,x)})"
    1.27  
    1.28 -  real_diff_def "x - y == x + (- y :: real)"
    1.29 +  real_diff_def
    1.30 +  "R - (S::real) == R + - S"
    1.31  
    1.32 +  real_inverse_def
    1.33 +  "inverse (R::real) == (@S. R ~= 0 & S*R = 1r)"
    1.34 +
    1.35 +  real_divide_def
    1.36 +  "R / (S::real) == R * inverse S"
    1.37 +  
    1.38  constdefs
    1.39  
    1.40    real_of_preal :: preal => real            
    1.41 @@ -42,9 +49,6 @@
    1.42             Abs_real(realrel^^{(m+preal_of_prat(prat_of_pnat 1p),
    1.43                                 preal_of_prat(prat_of_pnat 1p))})"
    1.44  
    1.45 -  rinv       :: real => real
    1.46 -  "rinv(R)   == (@S. R ~= 0 & S*R = 1r)"
    1.47 -
    1.48    real_of_posnat :: nat => real             
    1.49    "real_of_posnat n == real_of_preal(preal_of_prat(prat_of_pnat(pnat_of_nat n)))"
    1.50