src/HOL/Divides.thy
changeset 31998 2c7a24f74db9
parent 31952 40501bb2d57c
child 32010 cb1a1c94b4cd
     1.1 --- a/src/HOL/Divides.thy	Tue Jul 14 10:53:44 2009 +0200
     1.2 +++ b/src/HOL/Divides.thy	Tue Jul 14 10:54:04 2009 +0200
     1.3 @@ -131,7 +131,7 @@
     1.4    note that ultimately show thesis by blast
     1.5  qed
     1.6  
     1.7 -lemma dvd_eq_mod_eq_0 [code unfold]: "a dvd b \<longleftrightarrow> b mod a = 0"
     1.8 +lemma dvd_eq_mod_eq_0 [code_unfold]: "a dvd b \<longleftrightarrow> b mod a = 0"
     1.9  proof
    1.10    assume "b mod a = 0"
    1.11    with mod_div_equality [of b a] have "b div a * a = b" by simp