1.1 --- a/src/HOL/IntDiv.thy	Fri Oct 12 08:20:45 2007 +0200
     1.2 +++ b/src/HOL/IntDiv.thy	Fri Oct 12 08:20:46 2007 +0200
     1.3 @@ -1144,7 +1144,7 @@
     1.4    by (simp add: dvd_def zmod_eq_0_iff)
     1.5  
     1.6  instance int :: dvd_mod
     1.7 -  by default (simp add: times_class.dvd [symmetric] zdvd_iff_zmod_eq_0)
     1.8 +  by default (simp add: zdvd_iff_zmod_eq_0)
     1.9  
    1.10  lemmas zdvd_iff_zmod_eq_0_number_of [simp] =
    1.11    zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard]