src/HOL/Decision_Procs/Commutative_Ring.thy
changeset 58834 773b378d9313
parent 58770 ae5e9b4f8daf
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Thu Oct 30 16:36:44 2014 +0000
     1.2 +++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Thu Oct 30 21:02:01 2014 +0100
     1.3 @@ -269,7 +269,7 @@
     1.4          by (simp add: even_pow sqr_ci power_mult_distrib power_add [symmetric] mult_2 [symmetric] even_two_times_div_two)
     1.5      next
     1.6        case False with * show ?thesis
     1.7 -        by (simp add: odd_pow mul_ci sqr_ci power_mult_distrib power_add [symmetric] mult_2 [symmetric] power_Suc [symmetric] odd_two_times_div_two_Suc)
     1.8 +        by (simp add: odd_pow mul_ci sqr_ci power_mult_distrib power_add [symmetric] mult_2 [symmetric] power_Suc [symmetric])
     1.9      qed
    1.10    qed
    1.11  qed