src/HOL/Divides.thy

--- a/src/HOL/Divides.thy	Mon Feb 01 14:12:12 2010 +0100
+++ b/src/HOL/Divides.thy	Tue Feb 02 11:38:38 2010 +0100
@@ -2451,7 +2451,8 @@
     in subst [OF mod_div_equality [of _ n]])
    arith
 
-lemmas [nitpick_def] = mod_div_equality' [THEN eq_reflection]
+lemmas [nitpick_def] = dvd_eq_mod_eq_0 [THEN eq_reflection]
+                       mod_div_equality' [THEN eq_reflection]
                        zmod_zdiv_equality' [THEN eq_reflection]
 
 subsubsection {* Code generation *}