--- a/src/HOL/Real/real_arith.ML Wed May 04 08:37:45 2005 +0200
+++ b/src/HOL/Real/real_arith.ML Wed May 04 10:42:43 2005 +0200
@@ -118,11 +118,12 @@
Fast_Arith.lin_arith_prover;
val real_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_mono_thms,
inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
lessD = lessD, (*Can't change LA_Data_Ref.lessD: the reals are dense!*)
+ neqE = neqE,
simpset = simpset addsimps simps}),
arith_inj_const ("RealDef.real", HOLogic.natT --> HOLogic.realT),
arith_inj_const ("RealDef.real", HOLogic.intT --> HOLogic.realT),