diff -r 61bfaa892a41 -r 73de0ef7cb25 src/HOL/Integ/IntDiv.thy
--- a/src/HOL/Integ/IntDiv.thy	Wed Nov 13 15:36:36 2002 +0100
+++ b/src/HOL/Integ/IntDiv.thy	Fri Nov 15 18:02:25 2002 +0100
@@ -628,6 +628,8 @@
 
 declare zmod_eq_0_iff [THEN iffD1, dest!]
 
+lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
+by(simp add:dvd_def zmod_eq_0_iff)
 
 (** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **)