| changeset 31336 | e17f13cd1280 |
| parent 31017 | 2c227493ea56 |
| child 31338 | d41a8ba25b67 |
--- 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)