add [code del] declarations
authorhuffman
Mon Jun 01 07:57:37 2009 -0700 (2009-06-01)
changeset 3135314a58e2ca374
parent 31352 b3b534f06c2d
child 31354 2ad53771c30f
add [code del] declarations
src/HOL/Lim.thy
src/HOL/Limits.thy
src/HOL/SEQ.thy
     1.1 --- a/src/HOL/Lim.thy	Mon Jun 01 07:45:49 2009 -0700
     1.2 +++ b/src/HOL/Lim.thy	Mon Jun 01 07:57:37 2009 -0700
     1.3 @@ -14,7 +14,7 @@
     1.4  
     1.5  definition
     1.6    at :: "'a::metric_space \<Rightarrow> 'a filter" where
     1.7 -  "at a = Abs_filter (\<lambda>P. \<exists>r>0. \<forall>x. x \<noteq> a \<and> dist x a < r \<longrightarrow> P x)"
     1.8 +  [code del]: "at a = Abs_filter (\<lambda>P. \<exists>r>0. \<forall>x. x \<noteq> a \<and> dist x a < r \<longrightarrow> P x)"
     1.9  
    1.10  definition
    1.11    LIM :: "['a::metric_space \<Rightarrow> 'b::metric_space, 'a, 'b] \<Rightarrow> bool"
     2.1 --- a/src/HOL/Limits.thy	Mon Jun 01 07:45:49 2009 -0700
     2.2 +++ b/src/HOL/Limits.thy	Mon Jun 01 07:57:37 2009 -0700
     2.3 @@ -20,7 +20,7 @@
     2.4  
     2.5  definition
     2.6    eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool" where
     2.7 -  "eventually P F \<longleftrightarrow> Rep_filter F P"
     2.8 +  [simp del]: "eventually P F \<longleftrightarrow> Rep_filter F P"
     2.9  
    2.10  lemma eventually_True [simp]: "eventually (\<lambda>x. True) F"
    2.11  unfolding eventually_def using Rep_filter [of F] by blast
    2.12 @@ -85,7 +85,7 @@
    2.13  
    2.14  definition
    2.15    Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool" where
    2.16 -  "Zfun S F = (\<forall>r>0. eventually (\<lambda>i. norm (S i) < r) F)"
    2.17 +  [code del]: "Zfun S F = (\<forall>r>0. eventually (\<lambda>i. norm (S i) < r) F)"
    2.18  
    2.19  lemma ZfunI:
    2.20    "(\<And>r. 0 < r \<Longrightarrow> eventually (\<lambda>i. norm (S i) < r) F) \<Longrightarrow> Zfun S F"
    2.21 @@ -228,7 +228,7 @@
    2.22  
    2.23  definition
    2.24    tendsto :: "('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'b \<Rightarrow> 'a filter \<Rightarrow> bool" where
    2.25 -  "tendsto f l net \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
    2.26 +  [code del]: "tendsto f l net \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
    2.27  
    2.28  lemma tendstoI:
    2.29    "(\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net)
     3.1 --- a/src/HOL/SEQ.thy	Mon Jun 01 07:45:49 2009 -0700
     3.2 +++ b/src/HOL/SEQ.thy	Mon Jun 01 07:57:37 2009 -0700
     3.3 @@ -14,7 +14,7 @@
     3.4  
     3.5  definition
     3.6    sequentially :: "nat filter" where
     3.7 -  "sequentially = Abs_filter (\<lambda>P. \<exists>N. \<forall>n\<ge>N. P n)"
     3.8 +  [code del]: "sequentially = Abs_filter (\<lambda>P. \<exists>N. \<forall>n\<ge>N. P n)"
     3.9  
    3.10  definition
    3.11    Zseq :: "[nat \<Rightarrow> 'a::real_normed_vector] \<Rightarrow> bool" where