# HG changeset patch
# User haftmann
# Date 1239950091 -7200
# Node ID 207ec81543f6cb044c8ea208131629136f3d8d43
# Parent  c6c9359e474cf184bf61cd451cc90f5ba34d7af4
added both cancel_div_mod_procs

diff -r c6c9359e474c -r 207ec81543f6 src/HOL/Decision_Procs/cooper_tac.ML
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Thu Apr 16 14:10:58 2009 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Fri Apr 17 08:34:51 2009 +0200
@@ -76,7 +76,7 @@
 				  @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
 				  Suc_plus1]
 			addsimps @{thms add_ac}
-			addsimprocs [cancel_div_mod_proc]
+			addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
     val simpset0 = HOL_basic_ss
       addsimps [mod_div_equality', Suc_plus1]
       addsimps comp_arith
diff -r c6c9359e474c -r 207ec81543f6 src/HOL/Decision_Procs/mir_tac.ML
--- a/src/HOL/Decision_Procs/mir_tac.ML	Thu Apr 16 14:10:58 2009 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML	Fri Apr 17 08:34:51 2009 +0200
@@ -99,7 +99,7 @@
                                   @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
                                   @{thm "Suc_plus1"}]
                         addsimps @{thms add_ac}
-                        addsimprocs [cancel_div_mod_proc]
+                        addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
     val simpset0 = HOL_basic_ss
       addsimps [mod_div_equality', Suc_plus1]
       addsimps comp_ths