--- a/src/HOL/Integ/NatBin.thy Tue May 03 15:37:41 2005 +0200
+++ b/src/HOL/Integ/NatBin.thy Wed May 04 08:36:10 2005 +0200
@@ -565,10 +565,10 @@
val nat_bin_arith_setup =
[Fast_Arith.map_data
- (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
+ (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
{add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
inj_thms = inj_thms,
- lessD = lessD,
+ lessD = lessD, neqE = neqE,
simpset = simpset addsimps [Suc_nat_number_of, int_nat_number_of,
not_neg_number_of_Pls,
neg_number_of_Min,neg_number_of_BIT]})]