src/HOL/ex/Dedekind_Real.thy
changeset 39910 10097e0a9dbd
parent 37765 26bdfb7b680b
child 40822 98a5faa5aec0
     1.1 --- a/src/HOL/ex/Dedekind_Real.thy	Fri Oct 01 14:15:49 2010 +0200
     1.2 +++ b/src/HOL/ex/Dedekind_Real.thy	Fri Oct 01 16:05:25 2010 +0200
     1.3 @@ -1183,11 +1183,11 @@
     1.4  
     1.5  definition
     1.6    real_add_def: "z + w =
     1.7 -       contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
     1.8 +       the_elem (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
     1.9                   { Abs_Real(realrel``{(x+u, y+v)}) })"
    1.10  
    1.11  definition
    1.12 -  real_minus_def: "- r =  contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
    1.13 +  real_minus_def: "- r =  the_elem (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
    1.14  
    1.15  definition
    1.16    real_diff_def: "r - (s::real) = r + - s"
    1.17 @@ -1195,7 +1195,7 @@
    1.18  definition
    1.19    real_mult_def:
    1.20      "z * w =
    1.21 -       contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
    1.22 +       the_elem (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
    1.23                   { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })"
    1.24  
    1.25  definition