--- a/src/HOL/Decision_Procs/cooper_tac.ML Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Sat Dec 17 15:22:14 2016 +0100
@@ -45,8 +45,8 @@
(* Some simpsets for dealing with mod div abs and nat*)
val mod_div_simpset =
put_simpset HOL_basic_ss ctxt
- addsimps @{thms refl mod_add_eq [symmetric] mod_add_left_eq [symmetric]
- mod_add_right_eq [symmetric]
+ addsimps @{thms refl mod_add_eq mod_add_left_eq
+ mod_add_right_eq
div_add1_eq [symmetric] zdiv_zadd1_eq [symmetric]
mod_self
div_by_0 mod_by_0 div_0 mod_0