# HG changeset patch
# User huffman
# Date 1244050151 25200
# Node ID 74fc28c5d68c37d9de5d07ca496dc35948821dc5
# Parent  9baa48bad81c99bd5e1a9b3ac0600e7d8e5eb05e
more [code del] declarations

diff -r 9baa48bad81c -r 74fc28c5d68c src/HOL/Complex.thy
--- 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
diff -r 9baa48bad81c -r 74fc28c5d68c src/HOL/RealVector.thy
--- 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