src/HOL/Transcendental.thy
changeset 59647 c6f413b660cf
parent 59613 7103019278f0
child 59658 0cc388370041
     1.1 --- a/src/HOL/Transcendental.thy	Sat Mar 07 15:40:36 2015 +0100
     1.2 +++ b/src/HOL/Transcendental.thy	Sat Mar 07 21:32:31 2015 +0100
     1.3 @@ -4028,11 +4028,12 @@
     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 -          by (rule suminf_eq_arctan_bounded[where x="0" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>", symmetric])
     1.8 +        thm suminf_eq_arctan_bounded
     1.9 +          by (rule suminf_eq_arctan_bounded[where x1="0" and a1="-\<bar>x\<bar>" and b1="\<bar>x\<bar>", symmetric])
    1.10              (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
    1.11          moreover
    1.12          have "suminf (?c x) - arctan x = suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>)"
    1.13 -          by (rule suminf_eq_arctan_bounded[where x="x" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>"])
    1.14 +          by (rule suminf_eq_arctan_bounded[where x1="x" and a1="-\<bar>x\<bar>" and b1="\<bar>x\<bar>"])
    1.15               (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
    1.16          ultimately
    1.17          show ?thesis using suminf_arctan_zero by auto