--- 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
--- 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