src/HOL/Tools/int_arith.ML
changeset 33296 a3924d1069e5
parent 32603 e08fdd615333
child 34974 18b41bba42b5
     1.1 --- a/src/HOL/Tools/int_arith.ML	Wed Oct 28 17:44:03 2009 +0100
     1.2 +++ b/src/HOL/Tools/int_arith.ML	Wed Oct 28 19:09:47 2009 +0100
     1.3 @@ -98,9 +98,7 @@
     1.4    #> Lin_Arith.add_lessD @{thm zless_imp_add1_zle}
     1.5    #> Lin_Arith.add_simps (@{thms simp_thms} @ @{thms arith_simps} @ @{thms rel_simps}
     1.6        @ @{thms arith_special} @ @{thms int_arith_rules})
     1.7 -  #> Lin_Arith.add_simprocs (Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc
     1.8 -      :: Numeral_Simprocs.combine_numerals
     1.9 -      :: Numeral_Simprocs.cancel_numerals)
    1.10 +  #> Lin_Arith.add_simprocs [zero_one_idom_simproc]
    1.11    #> Lin_Arith.set_number_of number_of
    1.12    #> Lin_Arith.add_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT)
    1.13    #> Lin_Arith.add_discrete_type @{type_name Int.int}