changeset 40077 | c8a9eaaa2f59 |
parent 33356 | 9157d0f9f00e |
child 41807 | ab5d2d81f9fb |
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy Fri Oct 22 23:45:20 2010 +0200 +++ b/src/HOL/Decision_Procs/Commutative_Ring.thy Sun Oct 24 20:19:00 2010 +0200 @@ -266,7 +266,7 @@ proof cases assume "even l" then have "Suc l div 2 = l div 2" - by (simp add: nat_number even_nat_plus_one_div_two) + by (simp add: eval_nat_numeral even_nat_plus_one_div_two) moreover from Suc have "l < k" by simp with 1 have "\<And>P. Ipol ls (pow l P) = Ipol ls P ^ l" by simp