--- a/src/HOL/RealVector.thy Mon Jul 12 08:58:27 2010 +0200
+++ b/src/HOL/RealVector.thy Mon Jul 12 10:48:37 2010 +0200
@@ -305,9 +305,8 @@
subsection {* The Set of Real Numbers *}
-definition
- Reals :: "'a::real_algebra_1 set" where
- [code del]: "Reals = range of_real"
+definition Reals :: "'a::real_algebra_1 set" where
+ "Reals = range of_real"
notation (xsymbols)
Reals ("\<real>")
@@ -786,7 +785,7 @@
definition dist_real_def:
"dist x y = \<bar>x - y\<bar>"
-definition open_real_def [code del]:
+definition open_real_def:
"open (S :: real set) \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
instance