src/HOL/Tools/int_arith.ML
changeset 31082 54a442b2d727
parent 31068 f591144b0f17
child 31100 6a2e67fe4488
     1.1 --- a/src/HOL/Tools/int_arith.ML	Fri May 08 13:38:21 2009 +0200
     1.2 +++ b/src/HOL/Tools/int_arith.ML	Sat May 09 09:17:29 2009 +0200
     1.3 @@ -93,15 +93,14 @@
     1.4  val setup =
     1.5    Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
     1.6     {add_mono_thms = add_mono_thms,
     1.7 -    mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: mult_mono_thms,
     1.8 +    mult_mono_thms = (*@{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: *)mult_mono_thms,
     1.9      inj_thms = nat_inj_thms @ inj_thms,
    1.10      lessD = lessD @ [@{thm zless_imp_add1_zle}],
    1.11      neqE = neqE,
    1.12      simpset = simpset addsimps add_rules
    1.13 -                      addsimprocs numeral_base_simprocs
    1.14 -                      addcongs [if_weak_cong]}) #>
    1.15 -  arith_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) #>
    1.16 -  arith_discrete @{type_name Int.int}
    1.17 +                      addsimprocs numeral_base_simprocs}) #>
    1.18 +  Lin_Arith.add_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) #>
    1.19 +  Lin_Arith.add_discrete_type @{type_name Int.int}
    1.20  
    1.21  val fast_int_arith_simproc =
    1.22    Simplifier.simproc (the_context ())