src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
changeset 58834 773b378d9313
parent 58776 95e58e04e534
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Oct 30 16:36:44 2014 +0000
     1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Oct 30 21:02:01 2014 +0100
     1.3 @@ -790,7 +790,7 @@
     1.4      also have "\<dots> = (Ipoly bs p) ^ (Suc (Suc (Suc 0) * (Suc n div Suc (Suc 0))))"
     1.5        by (simp only: th)
     1.6      finally have ?case unfolding numeral_2_eq_2 [symmetric]
     1.7 -    using odd_two_times_div_two_Suc [OF odd] by simp
     1.8 +    using odd_two_times_div_two_nat [OF odd] by simp
     1.9    }
    1.10    moreover
    1.11    {