src/HOL/Transcendental.thy
changeset 58834 773b378d9313
parent 58740 cb9d84d3e7f2
child 58889 5b7a9633cfa8
--- a/src/HOL/Transcendental.thy	Thu Oct 30 16:36:44 2014 +0000
+++ b/src/HOL/Transcendental.thy	Thu Oct 30 21:02:01 2014 +0100
@@ -203,7 +203,7 @@
       then show ?thesis by (auto simp add: even_two_times_div_two)
     next
       case False
-      then have eq: "Suc (2 * (m div 2)) = m" by (simp add: odd_two_times_div_two_Suc)
+      then have eq: "Suc (2 * (m div 2)) = m" by simp
       hence "even (2 * (m div 2))" using `odd m` by auto
       have "?SUM m = ?SUM (Suc (2 * (m div 2)))" unfolding eq ..
       also have "\<dots> = ?SUM (2 * (m div 2))" using `even (2 * (m div 2))` by auto