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
```