# HG changeset patch
# User haftmann
# Date 1265634418 -3600
# Node ID a1d93ce94235457a62cd2954c8070133e021a299
# Parent  748f0bc3f7caa071f55cb148ea8d55e7fe8be168
more precise proofs

diff -r 748f0bc3f7ca -r a1d93ce94235 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Mon Feb 08 14:06:54 2010 +0100
+++ b/src/HOL/Transcendental.thy	Mon Feb 08 14:06:58 2010 +0100
@@ -2904,10 +2904,12 @@
     next
       case False hence "0 < \<bar>x\<bar>" and "- \<bar>x\<bar> < \<bar>x\<bar>" by auto
       have "suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>) = suminf (?c 0) - arctan 0"
-        by (rule suminf_eq_arctan_bounded[where x="0" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>", symmetric], auto simp add: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>`)
+        by (rule suminf_eq_arctan_bounded[where x="0" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>", symmetric])
+          (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
       moreover
       have "suminf (?c x) - arctan x = suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>)"
-        by (rule suminf_eq_arctan_bounded[where x="x" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>"], auto simp add: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>`)
+        by (rule suminf_eq_arctan_bounded[where x="x" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>"])
+          (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
       ultimately 
       show ?thesis using suminf_arctan_zero by auto
     qed