src/HOL/Lim.thy
changeset 31353 14a58e2ca374
parent 31349 2261c8781f73
child 31355 3d18766ddc4b
     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"