src/HOL/Tools/int_arith.ML
changeset 47209 4893907fe872
parent 47108 2a1953f0d20d
child 51717 9e7d1c139569
     1.1 --- a/src/HOL/Tools/int_arith.ML	Fri Mar 30 08:11:52 2012 +0200
     1.2 +++ b/src/HOL/Tools/int_arith.ML	Fri Mar 30 09:08:29 2012 +0200
     1.3 @@ -86,6 +86,7 @@
     1.4    Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
     1.5    #> Lin_Arith.add_lessD @{thm zless_imp_add1_zle}
     1.6    #> Lin_Arith.add_simps (@{thms simp_thms} @ @{thms arith_simps} @ @{thms rel_simps}
     1.7 +      @ @{thms pred_numeral_simps}
     1.8        @ @{thms arith_special} @ @{thms int_arith_rules})
     1.9    #> Lin_Arith.add_simprocs [zero_one_idom_simproc]
    1.10    #> Lin_Arith.set_number_of number_of