--- a/src/HOL/Limits.thy Mon Jun 01 10:56:31 2009 -0700
+++ b/src/HOL/Limits.thy Mon Jun 01 16:27:54 2009 -0700
@@ -85,7 +85,7 @@
definition
Bfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool" where
- "Bfun S F = (\<exists>K>0. eventually (\<lambda>i. norm (S i) \<le> K) F)"
+ [code del]: "Bfun S F = (\<exists>K>0. eventually (\<lambda>i. norm (S i) \<le> K) F)"
lemma BfunI: assumes K: "eventually (\<lambda>i. norm (X i) \<le> K) F" shows "Bfun X F"
unfolding Bfun_def