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