# HG changeset patch
# User haftmann
# Date 1371309563 -7200
# Node ID 63eec9cea2c7660d0f8746626543a98c354c9c47
# Parent  3cc46b8cca5efb5f68311b5ac1b2740c9c7c3d7d
pragmatic executability for instance real :: open

diff -r 3cc46b8cca5e -r 63eec9cea2c7 src/HOL/Real_Vector_Spaces.thy
--- 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
+