--- a/src/HOL/Real_Vector_Spaces.thy Sat Jun 15 17:19:23 2013 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Sat Jun 15 17:19:23 2013 +0200
@@ -807,7 +807,7 @@
definition dist_real_def:
"dist x y = \<bar>x - y\<bar>"
-definition open_real_def:
+definition open_real_def [code del]:
"open (S :: real set) \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
definition real_norm_def [simp]:
@@ -826,6 +826,8 @@
end
+code_abort "open :: real set \<Rightarrow> bool"
+
instance real :: linorder_topology
proof
show "(open :: real set \<Rightarrow> bool) = generate_topology (range lessThan \<union> range greaterThan)"
@@ -1543,3 +1545,4 @@
qed
end
+