src/HOL/Divides.thy
changeset 34982 7b8c366e34a2
parent 34225 21c5405deb6b
child 35050 9f841f20dca6
     1.1 --- a/src/HOL/Divides.thy	Mon Feb 01 14:12:12 2010 +0100
     1.2 +++ b/src/HOL/Divides.thy	Tue Feb 02 11:38:38 2010 +0100
     1.3 @@ -2451,7 +2451,8 @@
     1.4      in subst [OF mod_div_equality [of _ n]])
     1.5     arith
     1.6  
     1.7 -lemmas [nitpick_def] = mod_div_equality' [THEN eq_reflection]
     1.8 +lemmas [nitpick_def] = dvd_eq_mod_eq_0 [THEN eq_reflection]
     1.9 +                       mod_div_equality' [THEN eq_reflection]
    1.10                         zmod_zdiv_equality' [THEN eq_reflection]
    1.11  
    1.12  subsubsection {* Code generation *}