# HG changeset patch
# User huffman
# Date 1313424497 25200
# Node ID 00d3147dd6390ae08a3f46e59dfc616a6c4adf49
# Parent  1d2bf1f240ac3cd70b86eab23412c0f868287e34
simplify some proofs

diff -r 1d2bf1f240ac -r 00d3147dd639 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Sun Aug 14 13:04:57 2011 -0700
+++ b/src/HOL/Deriv.thy	Mon Aug 15 09:08:17 2011 -0700
@@ -1601,29 +1601,26 @@
 lemma LIM_fun_gt_zero:
      "[| f -- c --> (l::real); 0 < l |]  
          ==> \<exists>r. 0 < r & (\<forall>x::real. x \<noteq> c & \<bar>c - x\<bar> < r --> 0 < f x)"
-apply (auto simp add: LIM_eq)
-apply (drule_tac x = "l/2" in spec, safe, force)
+apply (drule (1) LIM_D, clarify)
 apply (rule_tac x = s in exI)
-apply (auto simp only: abs_less_iff)
+apply (simp add: abs_less_iff)
 done
 
 lemma LIM_fun_less_zero:
      "[| f -- c --> (l::real); l < 0 |]  
       ==> \<exists>r. 0 < r & (\<forall>x::real. x \<noteq> c & \<bar>c - x\<bar> < r --> f x < 0)"
-apply (auto simp add: LIM_eq)
-apply (drule_tac x = "-l/2" in spec, safe, force)
+apply (drule LIM_D [where r="-l"], simp, clarify)
 apply (rule_tac x = s in exI)
-apply (auto simp only: abs_less_iff)
+apply (simp add: abs_less_iff)
 done
 
-
 lemma LIM_fun_not_zero:
      "[| f -- c --> (l::real); l \<noteq> 0 |] 
       ==> \<exists>r. 0 < r & (\<forall>x::real. x \<noteq> c & \<bar>c - x\<bar> < r --> f x \<noteq> 0)"
-apply (cut_tac x = l and y = 0 in linorder_less_linear, auto)
-apply (drule LIM_fun_less_zero)
-apply (drule_tac [3] LIM_fun_gt_zero)
-apply force+
+apply (rule linorder_cases [of l 0])
+apply (drule (1) LIM_fun_less_zero, force)
+apply simp
+apply (drule (1) LIM_fun_gt_zero, force)
 done
 
 end