| changeset 31998 | 2c7a24f74db9 |
| parent 31952 | 40501bb2d57c |
| child 32010 | cb1a1c94b4cd |
--- a/src/HOL/Divides.thy Tue Jul 14 10:53:44 2009 +0200 +++ b/src/HOL/Divides.thy Tue Jul 14 10:54:04 2009 +0200 @@ -131,7 +131,7 @@ note that ultimately show thesis by blast qed -lemma dvd_eq_mod_eq_0 [code unfold]: "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