# HG changeset patch
# User wenzelm
# Date 1426247056 -3600
# Node ID 6c896dfef33bf99025ec12ec4f187385de71cc09
# Parent  3baf9b3a24c761b2617173eae8cec8957c8785ca
removed junk;

diff -r 3baf9b3a24c7 -r 6c896dfef33b src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Fri Mar 13 11:47:42 2015 +0100
+++ b/src/HOL/Transcendental.thy	Fri Mar 13 12:44:16 2015 +0100
@@ -4363,7 +4363,6 @@
         case False
         hence "0 < \<bar>x\<bar>" and "- \<bar>x\<bar> < \<bar>x\<bar>" by auto
         have "suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>) = suminf (?c 0) - arctan 0"
-        thm suminf_eq_arctan_bounded
           by (rule suminf_eq_arctan_bounded[where x1="0" and a1="-\<bar>x\<bar>" and b1="\<bar>x\<bar>", symmetric])
             (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
         moreover