# HG changeset patch
# User huffman
# Date 1126827293 -7200
# Node ID 70311ad8bf114e30c1335add6b9132f5df508b32
# Parent  72325ec8fd8e908525417182967287f191f737af
fix names in hypreal_arith.ML

diff -r 72325ec8fd8e -r 70311ad8bf11 src/HOL/Hyperreal/NSA.thy
--- 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:
diff -r 72325ec8fd8e -r 70311ad8bf11 src/HOL/Hyperreal/hypreal_arith.ML
--- 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;