
diff -r 198eae6f5a35 -r e17f13cd1280 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Thu May 28 22:54:57 2009 -0700
+++ b/src/HOL/Deriv.thy	Thu May 28 22:57:17 2009 -0700
@@ -577,7 +577,7 @@
 apply (drule not_P_Bolzano_bisect', assumption+)
 apply (rename_tac "l")
 apply (drule_tac x = l in spec, clarify)
-apply (simp add: LIMSEQ_def)
+apply (simp add: LIMSEQ_iff)
 apply (drule_tac P = "%r. 0<r --> ?Q r" and x = "d/2" in spec)
 apply (drule_tac P = "%r. 0<r --> ?Q r" and x = "d/2" in spec)
 apply (drule real_less_half_sum, auto)




