src/HOL/Integ/int_arith1.ML
changeset 15184 d2c19aea17bc
parent 15013 34264f5e4691
child 15185 8c43ffe2bb32
     1.1 --- a/src/HOL/Integ/int_arith1.ML	Mon Sep 06 16:45:10 2004 +0200
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Mon Sep 06 17:37:35 2004 +0200
     1.3 @@ -516,7 +516,7 @@
     1.4  val int_arith_setup =
     1.5   [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
     1.6     {add_mono_thms = add_mono_thms,
     1.7 -    mult_mono_thms = mult_mono_thms,
     1.8 +    mult_mono_thms = [mult_strict_left_mono,mult_left_mono] @ mult_mono_thms,
     1.9      inj_thms = [zle_int RS iffD2,int_int_eq RS iffD2] @ inj_thms,
    1.10      lessD = lessD @ [zless_imp_add1_zle],
    1.11      simpset = simpset addsimps add_rules