--- a/src/HOL/Tools/Qelim/presburger.ML Sat Feb 21 09:58:45 2009 +0100
+++ b/src/HOL/Tools/Qelim/presburger.ML Sat Feb 21 20:52:30 2009 +0100
@@ -122,7 +122,7 @@
addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
val div_mod_ss = HOL_basic_ss addsimps simp_thms
@ map (symmetric o mk_meta_eq)
- [@{thm "dvd_eq_mod_eq_0"}, @{thm "zdvd_iff_zmod_eq_0"}, @{thm "mod_add1_eq"},
+ [@{thm "dvd_eq_mod_eq_0"}, @{thm "mod_add1_eq"},
@{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"},
@{thm "mod_add_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
@ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "mod_by_0"},