1.1 --- a/src/HOL/Divides.thy	Tue Mar 27 15:40:11 2012 +0200
     1.2 +++ b/src/HOL/Divides.thy	Tue Mar 27 15:53:48 2012 +0200
     1.3 @@ -1786,9 +1786,6 @@
     1.4  apply (blast intro: divmod_int_rel_div_mod [THEN zmult1_lemma, THEN div_int_unique])
     1.5  done
     1.6  
     1.7 -lemma zmod_zmult1_eq: "(a*b) mod c = a*(b mod c) mod (c::int)"
     1.8 -  by (fact mod_mult_right_eq) (* FIXME: delete *)
     1.9 -
    1.10  text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
    1.11  
    1.12  lemma zadd1_lemma: