# HG changeset patch
# User wenzelm
# Date 1319031763 -7200
# Node ID 78478d938cb8c269cbe5d434dc9dbdfa5f2d7de6
# Parent  63ce9e7437347d5d90ec16ee46f60421a9221104
inlined @{thms} (ML compile-time) allows to get rid of legacy zadd_ac as well (cf. 49e305100097);

diff -r 63ce9e743734 -r 78478d938cb8 NEWS
--- a/NEWS	Wed Oct 19 15:41:12 2011 +0200
+++ b/NEWS	Wed Oct 19 15:42:43 2011 +0200
@@ -28,6 +28,7 @@
   zadd_commute ~> add_commute
   zadd_assoc ~> add_assoc
   zadd_left_commute ~> add_left_commute
+  zadd_ac ~> add_ac
   zmult_ac ~> mult_ac
   zadd_0 ~> add_0_left
   zadd_0_right ~> add_0_right
diff -r 63ce9e743734 -r 78478d938cb8 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Wed Oct 19 15:41:12 2011 +0200
+++ b/src/HOL/Int.thy	Wed Oct 19 15:42:43 2011 +0200
@@ -2390,9 +2390,6 @@
 
 subsection {* Legacy theorems *}
 
-(* used by Tools/Qelim/cooper.ML *)
-lemmas zadd_ac = add_ac [where 'a=int]
-
 lemmas inj_int = inj_of_nat [where 'a=int]
 lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
 lemmas int_mult = of_nat_mult [where 'a=int]
diff -r 63ce9e743734 -r 78478d938cb8 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Wed Oct 19 15:41:12 2011 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Wed Oct 19 15:42:43 2011 +0200
@@ -74,7 +74,8 @@
 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 :: @{thms zadd_ac});
+val lin_ss =
+  presburger_ss addsimps (@{thm dvd_eq_mod_eq_0} :: zdvd1_eq :: @{thms add_ac [where 'a=int]});
 
 val iT = HOLogic.intT
 val bT = HOLogic.boolT;