1.1 --- a/src/HOL/Decision_Procs/mir_tac.ML Wed Jun 29 16:31:50 2011 +0200
1.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML Wed Jun 29 17:35:46 2011 +0200
1.3 @@ -104,7 +104,7 @@
1.4 @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
1.5 @{thm "Suc_eq_plus1"}]
1.6 addsimps @{thms add_ac}
1.7 - addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
1.8 + addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
1.9 val simpset0 = HOL_basic_ss
1.10 addsimps [mod_div_equality', @{thm Suc_eq_plus1}]
1.11 addsimps comp_ths