changeset 67091 | 1393c2340eec |
parent 66806 | a4e82b58d833 |
child 69593 | 3dda49e08b9d |
--- a/src/HOL/Numeral_Simprocs.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Numeral_Simprocs.thy Sun Nov 26 21:08:32 2017 +0100 @@ -77,7 +77,7 @@ by auto lemma nat_mult_dvd_cancel_disj[simp]: - "(k*m) dvd (k*n) = (k=0 | m dvd (n::nat))" + "(k*m) dvd (k*n) = (k=0 \<or> m dvd (n::nat))" by (auto simp: dvd_eq_mod_eq_0 mod_mult_mult1) lemma nat_mult_dvd_cancel1: "0 < k \<Longrightarrow> (k*m) dvd (k*n::nat) = (m dvd n)"