| changeset 31419 | 74fc28c5d68c |
| parent 31417 | c12b25b7f015 |
| child 31446 | 2d91b2416de8 |
--- a/src/HOL/RealVector.thy Wed Jun 03 10:02:59 2009 -0700 +++ b/src/HOL/RealVector.thy Wed Jun 03 10:29:11 2009 -0700 @@ -537,7 +537,7 @@ definition dist_real_def: "dist x y = \<bar>x - y\<bar>" -definition topo_real_def: +definition topo_real_def [code del]: "topo = {S::real set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}" instance