--- a/src/HOL/Hyperreal/NSA.thy Thu Sep 15 23:53:33 2005 +0200
+++ b/src/HOL/Hyperreal/NSA.thy Fri Sep 16 01:34:53 2005 +0200
@@ -1432,9 +1432,8 @@
"[| x < y; u \<in> Infinitesimal |]
==> hypreal_of_real x + u < hypreal_of_real y"
apply (simp add: Infinitesimal_def)
-apply (drule_tac x = "hypreal_of_real y + -hypreal_of_real x" in bspec, simp)
-apply (auto simp add: add_commute abs_less_iff SReal_minus)
-apply (simp add: compare_rls)
+apply (drule_tac x = "hypreal_of_real y + -hypreal_of_real x" in bspec, simp)
+apply (simp add: abs_less_iff)
done
lemma Infinitesimal_add_hrabs_hypreal_of_real_less:
--- a/src/HOL/Hyperreal/hypreal_arith.ML Thu Sep 15 23:53:33 2005 +0200
+++ b/src/HOL/Hyperreal/hypreal_arith.ML Fri Sep 16 01:34:53 2005 +0200
@@ -19,7 +19,7 @@
in
-val hyprealT = Type("Rational.hypreal", []);
+val hyprealT = Type("StarDef.star", [HOLogic.realT]);
val fast_hypreal_arith_simproc =
Simplifier.simproc (Theory.sign_of (the_context ()))
@@ -35,7 +35,7 @@
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),
+ arith_inj_const ("StarDef.star_of", HOLogic.realT --> hyprealT),
Simplifier.change_simpset_of (op addsimprocs) [fast_hypreal_arith_simproc]];
end;