src/HOL/Real/RealDef.thy

 uses ("real_arith.ML")
 begin
 
 definition
   realrel   ::  "((preal * preal) * (preal * preal)) set" where
-  [code func del]: "realrel = {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
+  [code del]: "realrel = {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
 
 typedef (Real)  real = "UNIV//realrel"
   by (auto simp add: quotient_def)
 
 definition
   (** these don't use the overloaded "real" function: users don't see them **)
   real_of_preal :: "preal => real" where
-  [code func del]: "real_of_preal m = Abs_Real (realrel `` {(m + 1, 1)})"
+  [code del]: "real_of_preal m = Abs_Real (realrel `` {(m + 1, 1)})"
 
 instantiation real :: "{zero, one, plus, minus, uminus, times, inverse, ord, abs, sgn}"
 begin
 
 definition
-  real_zero_def [code func del]: "0 = Abs_Real(realrel``{(1, 1)})"
-
-definition
-  real_one_def [code func del]: "1 = Abs_Real(realrel``{(1 + 1, 1)})"
-
-definition
-  real_add_def [code func del]: "z + w =
+  real_zero_def [code del]: "0 = Abs_Real(realrel``{(1, 1)})"
+
+definition
+  real_one_def [code del]: "1 = Abs_Real(realrel``{(1 + 1, 1)})"
+
+definition
+  real_add_def [code del]: "z + w =
        contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
                  { Abs_Real(realrel``{(x+u, y+v)}) })"
 
 definition
-  real_minus_def [code func del]: "- r =  contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
-
-definition
-  real_diff_def [code func del]: "r - (s::real) = r + - s"
-
-definition
-  real_mult_def [code func del]:
+  real_minus_def [code del]: "- r =  contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
+
+definition
+  real_diff_def [code del]: "r - (s::real) = r + - s"
+
+definition
+  real_mult_def [code del]:
     "z * w =
        contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
                  { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })"
 
 definition
-  real_inverse_def [code func del]: "inverse (R::real) = (THE S. (R = 0 & S = 0) | S * R = 1)"
-
-definition
-  real_divide_def [code func del]: "R / (S::real) = R * inverse S"
-
-definition
-  real_le_def [code func del]: "z \<le> (w::real) \<longleftrightarrow>
+  real_inverse_def [code del]: "inverse (R::real) = (THE S. (R = 0 & S = 0) | S * R = 1)"
+
+definition
+  real_divide_def [code del]: "R / (S::real) = R * inverse S"
+
+definition
+  real_le_def [code del]: "z \<le> (w::real) \<longleftrightarrow>
     (\<exists>x y u v. x+v \<le> u+y & (x,y) \<in> Rep_Real z & (u,v) \<in> Rep_Real w)"
 
 definition
-  real_less_def [code func del]: "x < (y\<Colon>real) \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
+  real_less_def [code del]: "x < (y\<Colon>real) \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
 
 definition
   real_abs_def:  "abs (r::real) = (if r < 0 then - r else r)"
 
 definition

 
 instantiation real :: number_ring
 begin
 
 definition
-  real_number_of_def [code func del]: "number_of w = real_of_int w"
+  real_number_of_def [code del]: "number_of w = real_of_int w"
 
 instance
   by intro_classes (simp add: real_number_of_def)
 
 end