changeset 50346 | a75c6429c3c3 |
parent 50331 | 4b6dc5077e98 |
child 50347 | 77e3effa50b6 |
--- a/src/HOL/Deriv.thy Tue Dec 04 16:20:24 2012 +0100 +++ b/src/HOL/Deriv.thy Tue Dec 04 18:00:31 2012 +0100 @@ -1783,7 +1783,7 @@ moreover have "eventually (\<lambda>t. 0 < g t) (at_right 0)" "eventually (\<lambda>t. g a < g t) (at_right 0)" - using g_0 by (auto elim: eventually_elim1 simp: filterlim_at_top) + using g_0 by (auto elim: eventually_elim1 simp: filterlim_at_top_dense) moreover have inv_g: "((\<lambda>x. inverse (g x)) ---> 0) (at_right 0)"