src/HOL/Transcendental.thy
changeset 56261 918432e3fcfa
parent 56217 dc429a5b13c4
child 56371 fb9ae0727548
     1.1 --- a/src/HOL/Transcendental.thy	Sun Mar 23 16:40:35 2014 +0100
     1.2 +++ b/src/HOL/Transcendental.thy	Mon Mar 24 14:22:29 2014 +0000
     1.3 @@ -3745,7 +3745,7 @@
     1.4              have "DERIV (\<lambda> x. suminf (?c x)) x :> (inverse (1 + x\<^sup>2))"
     1.5                unfolding suminf_c'_eq_geom
     1.6                by (rule DERIV_arctan_suminf[OF `0 < r` `r < 1` `\<bar>x\<bar> < r`])
     1.7 -            from DERIV_add_minus[OF this DERIV_arctan]
     1.8 +            from DERIV_diff [OF this DERIV_arctan]
     1.9              show "DERIV (\<lambda> x. suminf (?c x) - arctan x) x :> 0"
    1.10                by auto
    1.11            qed