1.1 --- a/src/HOL/Word/WordShift.thy	Sat Feb 21 09:58:45 2009 +0100
     1.2 +++ b/src/HOL/Word/WordShift.thy	Sat Feb 21 20:52:30 2009 +0100
     1.3 @@ -530,7 +530,7 @@
     1.4    done
     1.5  
     1.6  lemma and_mask_dvd: "2 ^ n dvd uint w = (w AND mask n = 0)"
     1.7 -  apply (simp add: zdvd_iff_zmod_eq_0 and_mask_mod_2p)
     1.8 +  apply (simp add: dvd_eq_mod_eq_0 and_mask_mod_2p)
     1.9    apply (simp add: word_uint.norm_eq_iff [symmetric] word_of_int_homs)
    1.10    apply (subst word_uint.norm_Rep [symmetric])
    1.11    apply (simp only: bintrunc_bintrunc_min bintrunc_mod2p [symmetric] min_def)