# 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