--- a/src/HOL/Integ/int_arith1.ML Tue May 03 15:37:41 2005 +0200
+++ b/src/HOL/Integ/int_arith1.ML Wed May 04 08:36:10 2005 +0200
@@ -514,11 +514,12 @@
in
val int_arith_setup =
- [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
+ [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
{add_mono_thms = add_mono_thms,
mult_mono_thms = [mult_strict_left_mono,mult_left_mono] @ mult_mono_thms,
inj_thms = [zle_int RS iffD2,int_int_eq RS iffD2] @ inj_thms,
lessD = lessD @ [zless_imp_add1_zle],
+ neqE = thm "linorder_neqE_int" :: neqE,
simpset = simpset addsimps add_rules
addsimprocs simprocs
addcongs [if_weak_cong]}),