# HG changeset patch
# User huffman
# Date 1243898874 25200
# Node ID df6acdd9dd379eb65eb82224eb526ad455789063
# Parent  ec8b9b6c47dc70d807e61b63638365b48c26258d
declare Bfun_def [code del]

diff -r ec8b9b6c47dc -r df6acdd9dd37 src/HOL/Limits.thy
--- 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