Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
changeset 58834 773b378d9313
parent 58776 95e58e04e534
child 58889 5b7a9633cfa8 
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Oct 30 16:36:44 2014 +0000
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Oct 30 21:02:01 2014 +0100
@@ -790,7 +790,7 @@
     also have "\<dots> = (Ipoly bs p) ^ (Suc (Suc (Suc 0) * (Suc n div Suc (Suc 0))))"
       by (simp only: th)
     finally have ?case unfolding numeral_2_eq_2 [symmetric]
-    using odd_two_times_div_two_Suc [OF odd] by simp
+    using odd_two_times_div_two_nat [OF odd] by simp
   }
   moreover
   {
isabelle