src/HOL/Tools/int_arith.ML
changeset 54249 ce00f2fef556
parent 51717 9e7d1c139569
child 59582 0fbed69ff081
     1.1 --- a/src/HOL/Tools/int_arith.ML	Mon Nov 04 18:08:47 2013 +0100
     1.2 +++ b/src/HOL/Tools/int_arith.ML	Mon Nov 04 20:10:06 2013 +0100
     1.3 @@ -87,9 +87,9 @@
     1.4  val setup =
     1.5    Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
     1.6    #> Lin_Arith.add_lessD @{thm zless_imp_add1_zle}
     1.7 -  #> Lin_Arith.add_simps (@{thms simp_thms} @ @{thms arith_simps} @ @{thms rel_simps}
     1.8 -      @ @{thms pred_numeral_simps}
     1.9 -      @ @{thms arith_special} @ @{thms int_arith_rules})
    1.10 +  #> Lin_Arith.add_simps @{thms of_nat_simps of_int_simps}
    1.11 +  #> Lin_Arith.add_simps
    1.12 +      [@{thm of_int_numeral}, @{thm nat_0}, @{thm nat_1}, @{thm diff_nat_numeral}, @{thm nat_numeral}]
    1.13    #> Lin_Arith.add_simprocs [zero_one_idom_simproc]
    1.14    #> Lin_Arith.set_number_of number_of
    1.15    #> Lin_Arith.add_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT)