src/HOL/Transcendental.thy
changeset 59688 6c896dfef33b
parent 59669 de7792ea4090
child 59731 7fccaeec22f0
     1.1 --- a/src/HOL/Transcendental.thy	Fri Mar 13 11:47:42 2015 +0100
     1.2 +++ b/src/HOL/Transcendental.thy	Fri Mar 13 12:44:16 2015 +0100
     1.3 @@ -4363,7 +4363,6 @@
     1.4          case False
     1.5          hence "0 < \<bar>x\<bar>" and "- \<bar>x\<bar> < \<bar>x\<bar>" by auto
     1.6          have "suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>) = suminf (?c 0) - arctan 0"
     1.7 -        thm suminf_eq_arctan_bounded
     1.8            by (rule suminf_eq_arctan_bounded[where x1="0" and a1="-\<bar>x\<bar>" and b1="\<bar>x\<bar>", symmetric])
     1.9              (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
    1.10          moreover