Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Transcendental.thy
changeset 56261 918432e3fcfa
parent 56217 dc429a5b13c4
child 56371 fb9ae0727548 
--- a/src/HOL/Transcendental.thy	Sun Mar 23 16:40:35 2014 +0100
+++ b/src/HOL/Transcendental.thy	Mon Mar 24 14:22:29 2014 +0000
@@ -3745,7 +3745,7 @@
             have "DERIV (\<lambda> x. suminf (?c x)) x :> (inverse (1 + x\<^sup>2))"
               unfolding suminf_c'_eq_geom
               by (rule DERIV_arctan_suminf[OF `0 < r` `r < 1` `\<bar>x\<bar> < r`])
-            from DERIV_add_minus[OF this DERIV_arctan]
+            from DERIV_diff [OF this DERIV_arctan]
             show "DERIV (\<lambda> x. suminf (?c x) - arctan x) x :> 0"
               by auto
           qed
isabelle