# HG changeset patch
# User huffman
# Date 1181684342 -7200
# Node ID 86e3729405448c537cea80e1468bc10717b17ce3
# Parent  7bb5dc641158b79019ce64ae721084bcc241f15f
thm antiquotations

diff -r 7bb5dc641158 -r 86e372940544 src/HOL/Tools/Presburger/cooper.ML
--- a/src/HOL/Tools/Presburger/cooper.ML	Tue Jun 12 23:14:29 2007 +0200
+++ b/src/HOL/Tools/Presburger/cooper.ML	Tue Jun 12 23:39:02 2007 +0200
@@ -25,7 +25,7 @@
 val false_tm = @{cterm "False"};
 val zdvd1_eq = @{thm "zdvd1_eq"};
 val presburger_ss = @{simpset} addsimps [zdvd1_eq];
-val lin_ss = presburger_ss addsimps (@{thm "dvd_eq_mod_eq_0"}::zdvd1_eq::zadd_ac);
+val lin_ss = presburger_ss addsimps (@{thm "dvd_eq_mod_eq_0"}::zdvd1_eq::@{thms zadd_ac});
 (* Some types and constants *)
 val iT = HOLogic.intT
 val bT = HOLogic.boolT;
@@ -658,4 +658,4 @@
             (HOLogic.mk_Trueprop (term_of_qf ps vs (pa (qf_of_term ps vs t))))
     end;
 
-end;
\ No newline at end of file
+end;