src/HOL/Hyperreal/Transcendental.thy
changeset 15241 a3949068537e
parent 15234 ec91a90c604e
child 15251 bb6f072c8d10
     1.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Mon Oct 11 19:36:48 2004 +0200
     1.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Tue Oct 12 11:48:21 2004 +0200
     1.3 @@ -2589,8 +2589,8 @@
     1.4        ==> \<exists>r. 0 < r & (\<forall>x. x \<noteq> c & \<bar>c - x\<bar> < r --> f x \<noteq> 0)"
     1.5  apply (cut_tac x = l and y = 0 in linorder_less_linear, auto)
     1.6  apply (drule LIM_fun_less_zero)
     1.7 -apply (drule_tac [3] LIM_fun_gt_zero, auto)
     1.8 -apply (rule_tac [!] x = r in exI, auto)
     1.9 +apply (drule_tac [3] LIM_fun_gt_zero)
    1.10 +apply force+
    1.11  done
    1.12  
    1.13  ML