| changeset 29108 | 12ca66b887a0 |
| parent 28823 | dcbef866c9e2 |
| child 29252 | ea97aa6aeba2 |
--- a/src/HOL/Divides.thy Thu Dec 11 08:53:53 2008 +0100 +++ b/src/HOL/Divides.thy Thu Dec 11 08:56:02 2008 +0100 @@ -127,7 +127,7 @@ note that ultimately show thesis by blast qed -lemma dvd_eq_mod_eq_0 [code]: "a dvd b \<longleftrightarrow> b mod a = 0" +lemma dvd_eq_mod_eq_0 [code unfold]: "a dvd b \<longleftrightarrow> b mod a = 0" proof assume "b mod a = 0" with mod_div_equality [of b a] have "b div a * a = b" by simp