src/HOL/Limits.thy
changeset 31357 df6acdd9dd37
parent 31356 ec8b9b6c47dc
child 31392 69570155ddf8
--- 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