src/HOL/Real_Vector_Spaces.thy
changeset 52381 63eec9cea2c7
parent 51775 408d937c9486
child 53374 a14d2a854c02
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Sat Jun 15 17:19:23 2013 +0200
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Sat Jun 15 17:19:23 2013 +0200
     1.3 @@ -807,7 +807,7 @@
     1.4  definition dist_real_def:
     1.5    "dist x y = \<bar>x - y\<bar>"
     1.6  
     1.7 -definition open_real_def:
     1.8 +definition open_real_def [code del]:
     1.9    "open (S :: real set) \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
    1.10  
    1.11  definition real_norm_def [simp]:
    1.12 @@ -826,6 +826,8 @@
    1.13  
    1.14  end
    1.15  
    1.16 +code_abort "open :: real set \<Rightarrow> bool"
    1.17 +
    1.18  instance real :: linorder_topology
    1.19  proof
    1.20    show "(open :: real set \<Rightarrow> bool) = generate_topology (range lessThan \<union> range greaterThan)"
    1.21 @@ -1543,3 +1545,4 @@
    1.22  qed
    1.23  
    1.24  end
    1.25 +