src/HOL/Decision_Procs/cooper_tac.ML
changeset 61694 6571c78c9667
parent 60754 02924903a6fd
child 62348 9a5f43dac883
     1.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Tue Nov 17 12:01:19 2015 +0100
     1.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Tue Nov 17 12:32:08 2015 +0000
     1.3 @@ -61,8 +61,8 @@
     1.4      (* Simp rules for changing (n::int) to int n *)
     1.5      val simpset1 =
     1.6        put_simpset HOL_basic_ss ctxt
     1.7 -      addsimps @{thms zdvd_int} @
     1.8 -        map (fn r => r RS sym) @{thms int_numeral int_int_eq zle_int zless_int zadd_int zmult_int}
     1.9 +      addsimps @{thms zdvd_int} @ [@{thm "of_nat_add"}, @{thm "of_nat_mult"}] @
    1.10 +        map (fn r => r RS sym) @{thms int_numeral int_int_eq zle_int zless_int}
    1.11        |> Splitter.add_split @{thm zdiff_int_split}
    1.12      (*simp rules for elimination of int n*)
    1.13