src/HOL/Real/RealDef.thy

--- a/src/HOL/Real/RealDef.thy	Sat Sep 16 18:04:14 2006 +0200
+++ b/src/HOL/Real/RealDef.thy	Sat Sep 16 19:12:03 2006 +0200
@@ -30,16 +30,9 @@
   "real_of_preal m = Abs_Real(realrel``{(m + preal_of_rat 1, preal_of_rat 1)})"
 
 consts
-   (*Overloaded constant denoting the Real subset of enclosing
-     types such as hypreal and complex*)
-   Reals :: "'a set"
-
    (*overloaded constant for injecting other types into "real"*)
    real :: "'a => real"
 
-const_syntax (xsymbols)
-  Reals  ("\<real>")
-
 
 defs (overloaded)