--- a/src/HOL/Tools/Qelim/cooper.ML Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Sun Oct 16 09:31:05 2016 +0200
@@ -835,7 +835,7 @@
addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}])
val splits_ss =
simpset_of (put_simpset comp_ss @{context}
- addsimps [@{thm "div_mult_mod_eq'"}]
+ addsimps [@{thm minus_div_mult_eq_mod [symmetric]}]
|> fold Splitter.add_split
[@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"},
@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}])