# HG changeset patch
# User haftmann
# Date 1592296899 0
# Node ID 92de7d74b8f81be766e0650b2c09a2a85d7ae917
# Parent  12f455cc657325b01748f77e9b597baa4907e39f
more specific thm reference

diff -r 12f455cc6573 -r 92de7d74b8f8 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Sat Jun 13 14:17:34 2020 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Tue Jun 16 08:41:39 2020 +0000
@@ -71,11 +71,12 @@
 
 val true_tm = \<^cterm>\<open>True\<close>;
 val false_tm = \<^cterm>\<open>False\<close>;
-val zdvd1_eq = @{thm "zdvd1_eq"};
-val presburger_ss = simpset_of (\<^context> addsimps [zdvd1_eq]);
+val presburger_ss = simpset_of (\<^context> addsimps @{thms zdvd1_eq});
 val lin_ss =
   simpset_of (put_simpset presburger_ss \<^context>
-    addsimps (@{thm dvd_eq_mod_eq_0} :: zdvd1_eq :: @{thms ac_simps [where 'a=int]}));
+    addsimps (@{thms dvd_eq_mod_eq_0 add.assoc [where 'a = int] add.commute [where 'a = int] add.left_commute [where 'a = int]
+  mult.assoc [where 'a = int] mult.commute [where 'a = int] mult.left_commute [where 'a = int]
+}));
 
 val iT = HOLogic.intT
 val bT = HOLogic.boolT;