1.1 --- a/src/HOL/Divides.thy	Sun Feb 22 10:22:46 2009 +0100
     1.2 +++ b/src/HOL/Divides.thy	Sun Feb 22 11:30:57 2009 +0100
     1.3 @@ -178,6 +178,12 @@
     1.4  lemma dvd_div_mult_self: "a dvd b \<Longrightarrow> (b div a) * a = b"
     1.5  by (subst (2) mod_div_equality [of b a, symmetric]) (simp add:dvd_imp_mod_0)
     1.6  
     1.7 +lemma dvd_div_mult: "a dvd b \<Longrightarrow> (b div a) * c = b * c div a"
     1.8 +apply (cases "a = 0")
     1.9 + apply simp
    1.10 +apply (auto simp: dvd_def mult_assoc)
    1.11 +done
    1.12 +
    1.13  lemma div_dvd_div[simp]:
    1.14    "a dvd b \<Longrightarrow> a dvd c \<Longrightarrow> (b div a dvd c div a) = (b dvd c)"
    1.15  apply (cases "a = 0")