src/HOL/Divides.thy
changeset 41792 ff3cb0c418b7
parent 41550 efa734d9b221
child 43594 ef1ddc59b825
     1.1 --- a/src/HOL/Divides.thy	Mon Feb 21 10:42:29 2011 +0100
     1.2 +++ b/src/HOL/Divides.thy	Mon Feb 21 10:44:19 2011 +0100
     1.3 @@ -2470,9 +2470,7 @@
     1.4      in subst [OF mod_div_equality [of _ n]])
     1.5     arith
     1.6  
     1.7 -lemmas [nitpick_def] = dvd_eq_mod_eq_0 [THEN eq_reflection]
     1.8 -                       mod_div_equality' [THEN eq_reflection]
     1.9 -                       zmod_zdiv_equality' [THEN eq_reflection]
    1.10 +lemmas [nitpick_unfold] = dvd_eq_mod_eq_0 mod_div_equality' zmod_zdiv_equality'
    1.11  
    1.12  
    1.13  subsubsection {* Code generation *}