| changeset 47163 | 248376f8881d |
| parent 47108 | 2a1953f0d20d |
| child 47224 | 773fe2754b8c |
--- a/src/HOL/Parity.thy Tue Mar 27 15:40:11 2012 +0200 +++ b/src/HOL/Parity.thy Tue Mar 27 15:53:48 2012 +0200 @@ -74,7 +74,7 @@ lemma anything_times_even: "even (y::int) ==> even (x * y)" by algebra lemma odd_times_odd: "odd (x::int) ==> odd y ==> odd (x * y)" - by (simp add: even_def zmod_zmult1_eq) + by (simp add: even_def mod_mult_right_eq) lemma even_product[simp,presburger]: "even((x::int) * y) = (even x | even y)" apply (auto simp add: even_times_anything anything_times_even)