| changeset 29252 | ea97aa6aeba2 |
| parent 29223 | e09c53289830 |
| parent 29108 | 12ca66b887a0 |
| child 29403 | fe17df4e4ab3 |
--- a/src/HOL/Divides.thy Tue Dec 30 08:18:54 2008 +0100 +++ b/src/HOL/Divides.thy Tue Dec 30 11:10:01 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