src/HOL/ex/Dedekind_Real.thy
changeset 60429 d3d1e185cd63
parent 60352 d46de31a50c4
child 61076 bdc1e2f0a86a
     1.1 --- a/src/HOL/ex/Dedekind_Real.thy	Thu Jun 11 21:41:55 2015 +0100
     1.2 +++ b/src/HOL/ex/Dedekind_Real.thy	Fri Jun 12 08:53:23 2015 +0200
     1.3 @@ -102,7 +102,7 @@
     1.4    preal_inverse_def:
     1.5      "inverse R == Abs_preal (inverse_set (Rep_preal R))"
     1.6  
     1.7 -definition "divide R S = R * inverse (S\<Colon>preal)"
     1.8 +definition "R div S = R * inverse (S\<Colon>preal)"
     1.9  
    1.10  definition
    1.11    preal_one_def:
    1.12 @@ -1222,7 +1222,7 @@
    1.13    real_inverse_def: "inverse (R::real) = (THE S. (R = 0 & S = 0) | S * R = 1)"
    1.14  
    1.15  definition
    1.16 -  real_divide_def: "divide R (S::real) = R * inverse S"
    1.17 +  real_divide_def: "R div (S::real) = R * inverse S"
    1.18  
    1.19  definition
    1.20    real_le_def: "z \<le> (w::real) \<longleftrightarrow>