diff -r 17256fe71aca -r ad73fb6144cf src/HOL/Hyperreal/HyperNat.thy
--- a/src/HOL/Hyperreal/HyperNat.thy	Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy	Tue Sep 06 23:16:48 2005 +0200
@@ -692,24 +692,24 @@
 constdefs
   hypreal_of_hypnat :: "hypnat => hypreal"
    "hypreal_of_hypnat N  == 
-      Abs_hypreal(\<Union>X \<in> Rep_hypnat(N). hyprel``{%n::nat. real (X n)})"
+      Abs_star(\<Union>X \<in> Rep_hypnat(N). starrel``{%n::nat. real (X n)})"
 
 
 lemma HNat_hypreal_of_nat [simp]: "hypreal_of_nat N \<in> Nats"
 by (simp add: hypreal_of_nat_def) 
 
 (*WARNING: FRAGILE!*)
-lemma lemma_hyprel_FUFN:
-     "(Ya \<in> hyprel ``{%n. f(n)}) = ({n. f n = Ya n} \<in> FreeUltrafilterNat)"
+lemma lemma_starrel_FUFN:
+     "(Ya \<in> starrel ``{%n. f(n)}) = ({n. f n = Ya n} \<in> FreeUltrafilterNat)"
 by force
 
 lemma hypreal_of_hypnat:
       "hypreal_of_hypnat (Abs_hypnat(hypnatrel``{%n. X n})) =
-       Abs_hypreal(hyprel `` {%n. real (X n)})"
+       Abs_star(starrel `` {%n. real (X n)})"
 apply (simp add: hypreal_of_hypnat_def)
-apply (rule_tac f = Abs_hypreal in arg_cong)
+apply (rule_tac f = Abs_star in arg_cong)
 apply (auto elim: FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset] 
-       simp add: lemma_hyprel_FUFN)
+       simp add: lemma_starrel_FUFN)
 done
 
 lemma hypreal_of_hypnat_inject [simp]:
@@ -756,7 +756,7 @@
 apply (cases n)
 apply (auto simp add: hypreal_of_hypnat hypreal_inverse 
       HNatInfinite_FreeUltrafilterNat_iff Infinitesimal_FreeUltrafilterNat_iff2)
-apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
+apply (rule bexI, rule_tac [2] lemma_starrel_refl, auto)
 apply (drule_tac x = "m + 1" in spec, ultra)
 done