# HG changeset patch
# User haftmann
# Date 1481984533 -3600
# Node ID c1932a4a227f3d2fad4f569b4c75d0b4e04d1a14
# Parent  293ab573d03484d786bec68d75b2e175ed056a4a
tuned fact references

diff -r 293ab573d034 -r c1932a4a227f src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML	Sat Dec 17 15:22:13 2016 +0100
@@ -823,15 +823,13 @@
     |> fold Simplifier.add_cong [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}])
 val div_mod_ss =
   simpset_of (put_simpset HOL_basic_ss @{context}
-    addsimps @{thms simp_thms}
-    @ map (Thm.symmetric o mk_meta_eq) 
-      [@{thm "dvd_eq_mod_eq_0"},
-       @{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 "mod_by_0"}, @{thm "div_by_0"},
-       @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"},
-       @{thm "div_by_Suc_0"}, @{thm "mod_by_Suc_0"}, @{thm "Suc_eq_plus1"}]
-    @ @{thms ac_simps}
+    addsimps @{thms simp_thms
+      mod_eq_0_iff_dvd mod_add_left_eq [symmetric] mod_add_right_eq [symmetric]
+      mod_add_eq [symmetric] div_add1_eq [symmetric] zdiv_zadd1_eq [symmetric]
+      mod_self mod_by_0 div_by_0
+      div_0 mod_0 div_by_1 mod_by_1
+      div_by_Suc_0 mod_by_Suc_0 Suc_eq_plus1
+      ac_simps}
    addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}])
 val splits_ss =
   simpset_of (put_simpset comp_ss @{context}