src/HOL/Integ/int_arith1.ML
changeset 15921 b6e345548913
parent 15661 9ef583b08647
child 15965 f422f8283491
     1.1 --- a/src/HOL/Integ/int_arith1.ML	Tue May 03 15:37:41 2005 +0200
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Wed May 04 08:36:10 2005 +0200
     1.3 @@ -514,11 +514,12 @@
     1.4  in
     1.5  
     1.6  val int_arith_setup =
     1.7 - [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
     1.8 + [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
     1.9     {add_mono_thms = add_mono_thms,
    1.10      mult_mono_thms = [mult_strict_left_mono,mult_left_mono] @ mult_mono_thms,
    1.11      inj_thms = [zle_int RS iffD2,int_int_eq RS iffD2] @ inj_thms,
    1.12      lessD = lessD @ [zless_imp_add1_zle],
    1.13 +    neqE = thm "linorder_neqE_int" :: neqE,
    1.14      simpset = simpset addsimps add_rules
    1.15                        addsimprocs simprocs
    1.16                        addcongs [if_weak_cong]}),