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