1.1 --- a/src/HOL/IntDiv.thy	Tue Jul 24 19:46:44 2007 +0200
     1.2 +++ b/src/HOL/IntDiv.thy	Tue Jul 24 19:58:53 2007 +0200
     1.3 @@ -1231,6 +1231,11 @@
     1.4    thus ?thesis by blast
     1.5  qed
     1.6  
     1.7 +lemma zdvd_zmult_cancel_disj[simp]:
     1.8 +  "(k*m) dvd (k*n) = (k=0 | m dvd (n::int))"
     1.9 +by (auto simp: zdvd_zmult_mono dest: zdvd_mult_cancel)
    1.10 +
    1.11 +
    1.12  theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
    1.13    apply (simp split add: split_nat)
    1.14    apply (rule iffI)