src/HOL/Real/RealDef.thy
changeset 21404 eb85850d3eb7
parent 20554 c433e78d4203
child 22456 6070e48ecb78
     1.1 --- a/src/HOL/Real/RealDef.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/HOL/Real/RealDef.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -14,7 +14,7 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  realrel   ::  "((preal * preal) * (preal * preal)) set"
     1.8 +  realrel   ::  "((preal * preal) * (preal * preal)) set" where
     1.9    "realrel = {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
    1.10  
    1.11  typedef (Real)  real = "UNIV//realrel"
    1.12 @@ -26,7 +26,7 @@
    1.13  
    1.14    (** these don't use the overloaded "real" function: users don't see them **)
    1.15  
    1.16 -  real_of_preal :: "preal => real"
    1.17 +  real_of_preal :: "preal => real" where
    1.18    "real_of_preal m = Abs_Real(realrel``{(m + preal_of_rat 1, preal_of_rat 1)})"
    1.19  
    1.20  consts