src/HOL/Transcendental.thy
changeset 59731 7fccaeec22f0
parent 59730 b7c394c7a619
parent 59688 6c896dfef33b
child 59741 5b762cd73a8e
     1.1 --- a/src/HOL/Transcendental.thy	Mon Mar 16 15:30:00 2015 +0000
     1.2 +++ b/src/HOL/Transcendental.thy	Tue Mar 17 12:23:56 2015 +0000
     1.3 @@ -16,6 +16,9 @@
     1.4  lemma real_fact_nat [simp]: "real (fact n :: nat) = fact n"
     1.5    by (simp add: real_of_nat_def)
     1.6  
     1.7 +lemma real_fact_int [simp]: "real (fact n :: int) = fact n"
     1.8 +  by (metis of_int_of_nat_eq of_nat_fact real_of_int_def)
     1.9 +
    1.10  lemma root_test_convergence:
    1.11    fixes f :: "nat \<Rightarrow> 'a::banach"
    1.12    assumes f: "(\<lambda>n. root n (norm (f n))) ----> x" -- "could be weakened to lim sup"
    1.13 @@ -4372,7 +4375,6 @@
    1.14          case False
    1.15          hence "0 < \<bar>x\<bar>" and "- \<bar>x\<bar> < \<bar>x\<bar>" by auto
    1.16          have "suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>) = suminf (?c 0) - arctan 0"
    1.17 -        thm suminf_eq_arctan_bounded
    1.18            by (rule suminf_eq_arctan_bounded[where x1="0" and a1="-\<bar>x\<bar>" and b1="\<bar>x\<bar>", symmetric])
    1.19              (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
    1.20          moreover