src/HOL/IntDiv.thy
changeset 29981 7d0ed261b712
parent 29951 a70bc5190534
child 30031 bd786c37af84
     1.1 --- a/src/HOL/IntDiv.thy	Wed Feb 18 14:17:04 2009 -0800
     1.2 +++ b/src/HOL/IntDiv.thy	Wed Feb 18 15:01:53 2009 -0800
     1.3 @@ -1265,9 +1265,9 @@
     1.4    thus ?thesis by simp
     1.5  qed
     1.6  
     1.7 -lemma zdvd_zmult_cancel_disj[simp]:
     1.8 +lemma zdvd_zmult_cancel_disj:
     1.9    "(k*m) dvd (k*n) = (k=0 | m dvd (n::int))"
    1.10 -by (auto simp: zdvd_zmult_mono dest: zdvd_mult_cancel)
    1.11 +by (rule dvd_mult_cancel_left) (* already declared [simp] *)
    1.12  
    1.13  
    1.14  theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"