src/HOL/SEQ.thy
changeset 31353 14a58e2ca374
parent 31349 2261c8781f73
child 31355 3d18766ddc4b
     1.1 --- a/src/HOL/SEQ.thy	Mon Jun 01 07:45:49 2009 -0700
     1.2 +++ b/src/HOL/SEQ.thy	Mon Jun 01 07:57:37 2009 -0700
     1.3 @@ -14,7 +14,7 @@
     1.4  
     1.5  definition
     1.6    sequentially :: "nat filter" where
     1.7 -  "sequentially = Abs_filter (\<lambda>P. \<exists>N. \<forall>n\<ge>N. P n)"
     1.8 +  [code del]: "sequentially = Abs_filter (\<lambda>P. \<exists>N. \<forall>n\<ge>N. P n)"
     1.9  
    1.10  definition
    1.11    Zseq :: "[nat \<Rightarrow> 'a::real_normed_vector] \<Rightarrow> bool" where