Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add [code del] declarations
authorhuffman
Mon, 01 Jun 2009 07:57:37 -0700
changeset 31353 14a58e2ca374
parent 31352 b3b534f06c2d
child 31354 2ad53771c30f
add [code del] declarations
src/HOL/Lim.thy file | annotate | diff | comparison | revisions
src/HOL/Limits.thy file | annotate | diff | comparison | revisions
src/HOL/SEQ.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Lim.thy	Mon Jun 01 07:45:49 2009 -0700
+++ b/src/HOL/Lim.thy	Mon Jun 01 07:57:37 2009 -0700
@@ -14,7 +14,7 @@
 
 definition
   at :: "'a::metric_space \<Rightarrow> 'a filter" where
-  "at a = Abs_filter (\<lambda>P. \<exists>r>0. \<forall>x. x \<noteq> a \<and> dist x a < r \<longrightarrow> P x)"
+  [code del]: "at a = Abs_filter (\<lambda>P. \<exists>r>0. \<forall>x. x \<noteq> a \<and> dist x a < r \<longrightarrow> P x)"
 
 definition
   LIM :: "['a::metric_space \<Rightarrow> 'b::metric_space, 'a, 'b] \<Rightarrow> bool"
--- a/src/HOL/Limits.thy	Mon Jun 01 07:45:49 2009 -0700
+++ b/src/HOL/Limits.thy	Mon Jun 01 07:57:37 2009 -0700
@@ -20,7 +20,7 @@
 
 definition
   eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool" where
-  "eventually P F \<longleftrightarrow> Rep_filter F P"
+  [simp del]: "eventually P F \<longleftrightarrow> Rep_filter F P"
 
 lemma eventually_True [simp]: "eventually (\<lambda>x. True) F"
 unfolding eventually_def using Rep_filter [of F] by blast
@@ -85,7 +85,7 @@
 
 definition
   Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool" where
-  "Zfun S F = (\<forall>r>0. eventually (\<lambda>i. norm (S i) < r) F)"
+  [code del]: "Zfun S F = (\<forall>r>0. eventually (\<lambda>i. norm (S i) < r) F)"
 
 lemma ZfunI:
   "(\<And>r. 0 < r \<Longrightarrow> eventually (\<lambda>i. norm (S i) < r) F) \<Longrightarrow> Zfun S F"
@@ -228,7 +228,7 @@
 
 definition
   tendsto :: "('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'b \<Rightarrow> 'a filter \<Rightarrow> bool" where
-  "tendsto f l net \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
+  [code del]: "tendsto f l net \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
 
 lemma tendstoI:
   "(\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net)
--- a/src/HOL/SEQ.thy	Mon Jun 01 07:45:49 2009 -0700
+++ b/src/HOL/SEQ.thy	Mon Jun 01 07:57:37 2009 -0700
@@ -14,7 +14,7 @@
 
 definition
   sequentially :: "nat filter" where
-  "sequentially = Abs_filter (\<lambda>P. \<exists>N. \<forall>n\<ge>N. P n)"
+  [code del]: "sequentially = Abs_filter (\<lambda>P. \<exists>N. \<forall>n\<ge>N. P n)"
 
 definition
   Zseq :: "[nat \<Rightarrow> 'a::real_normed_vector] \<Rightarrow> bool" where
isabelle