--- a/src/HOL/Decision_Procs/cooper_tac.ML Tue Nov 17 12:01:19 2015 +0100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Tue Nov 17 12:32:08 2015 +0000
@@ -61,8 +61,8 @@
(* Simp rules for changing (n::int) to int n *)
val simpset1 =
put_simpset HOL_basic_ss ctxt
- addsimps @{thms zdvd_int} @
- map (fn r => r RS sym) @{thms int_numeral int_int_eq zle_int zless_int zadd_int zmult_int}
+ addsimps @{thms zdvd_int} @ [@{thm "of_nat_add"}, @{thm "of_nat_mult"}] @
+ map (fn r => r RS sym) @{thms int_numeral int_int_eq zle_int zless_int}
|> Splitter.add_split @{thm zdiff_int_split}
(*simp rules for elimination of int n*)