--- a/src/HOL/Complex.thy Wed Jun 03 10:02:59 2009 -0700
+++ b/src/HOL/Complex.thy Wed Jun 03 10:29:11 2009 -0700
@@ -281,7 +281,7 @@
definition dist_complex_def:
"dist x y = cmod (x - y)"
-definition topo_complex_def:
+definition topo_complex_def [code del]:
"topo = {S::complex set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
lemmas cmod_def = complex_norm_def
--- 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