more [code del] declarations
authorhuffman
Wed Jun 03 10:29:11 2009 -0700 (2009-06-03)
changeset 3141974fc28c5d68c
parent 31418 9baa48bad81c
child 31420 4c22ef11078b
more [code del] declarations
src/HOL/Complex.thy
src/HOL/RealVector.thy
     1.1 --- a/src/HOL/Complex.thy	Wed Jun 03 10:02:59 2009 -0700
     1.2 +++ b/src/HOL/Complex.thy	Wed Jun 03 10:29:11 2009 -0700
     1.3 @@ -281,7 +281,7 @@
     1.4  definition dist_complex_def:
     1.5    "dist x y = cmod (x - y)"
     1.6  
     1.7 -definition topo_complex_def:
     1.8 +definition topo_complex_def [code del]:
     1.9    "topo = {S::complex set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
    1.10  
    1.11  lemmas cmod_def = complex_norm_def
     2.1 --- a/src/HOL/RealVector.thy	Wed Jun 03 10:02:59 2009 -0700
     2.2 +++ b/src/HOL/RealVector.thy	Wed Jun 03 10:29:11 2009 -0700
     2.3 @@ -537,7 +537,7 @@
     2.4  definition dist_real_def:
     2.5    "dist x y = \<bar>x - y\<bar>"
     2.6  
     2.7 -definition topo_real_def:
     2.8 +definition topo_real_def [code del]:
     2.9    "topo = {S::real set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
    2.10  
    2.11  instance