src/HOL/Numeral_Simprocs.thy
changeset 47159 978c00c20a59
parent 47108 2a1953f0d20d
child 47255 30a1692557b0
     1.1 --- a/src/HOL/Numeral_Simprocs.thy	Tue Mar 27 14:49:56 2012 +0200
     1.2 +++ b/src/HOL/Numeral_Simprocs.thy	Tue Mar 27 15:27:49 2012 +0200
     1.3 @@ -72,7 +72,7 @@
     1.4  
     1.5  lemma nat_mult_dvd_cancel_disj[simp]:
     1.6    "(k*m) dvd (k*n) = (k=0 | m dvd (n::nat))"
     1.7 -by(auto simp: dvd_eq_mod_eq_0 mod_mult_distrib2[symmetric])
     1.8 +by (auto simp: dvd_eq_mod_eq_0 mod_mult_mult1)
     1.9  
    1.10  lemma nat_mult_dvd_cancel1: "0 < k \<Longrightarrow> (k*m) dvd (k*n::nat) = (m dvd n)"
    1.11  by(auto)