--- a/src/HOL/Hyperreal/hypreal_arith.ML Wed May 04 08:37:45 2005 +0200
+++ b/src/HOL/Hyperreal/hypreal_arith.ML Wed May 04 10:42:43 2005 +0200
@@ -28,11 +28,12 @@
Fast_Arith.lin_arith_prover;
val hypreal_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 = inj_thms @ real_inj_thms,
lessD = lessD, (*Can't change LA_Data_Ref.lessD: the hypreals are dense!*)
+ neqE = neqE,
simpset = simpset}),
arith_inj_const ("HyperDef.hypreal_of_real", HOLogic.realT --> hyprealT),
Simplifier.change_simpset_of (op addsimprocs) [fast_hypreal_arith_simproc]];