# HG changeset patch
# User huffman
# Date 1126041408 -7200
# Node ID ad73fb6144cf0b0f128cc83870559941eda67505
# Parent  17256fe71aca51c3c5d0d5557c61cd54b66c0863
replace type hypreal with real star

diff -r 17256fe71aca -r ad73fb6144cf src/HOL/Complex/CLim.thy
--- a/src/HOL/Complex/CLim.thy	Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Complex/CLim.thy	Tue Sep 06 23:16:48 2005 +0200
@@ -126,7 +126,7 @@
 apply (rule_tac z = xa in eq_Abs_hcomplex)
 apply (auto simp add: hcomplex_of_complex_def starfunC hcomplex_diff 
          CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff)
-apply (rule bexI, rule_tac [2] lemma_hyprel_refl, safe)
+apply (rule bexI, rule_tac [2] lemma_starrel_refl, safe)
 apply (drule_tac x = u in spec, auto)
 apply (drule_tac x = s in spec, auto, ultra)
 apply (drule sym, auto)
@@ -196,8 +196,9 @@
 apply (auto simp add: hcomplex_of_complex_def starfunCR hcomplex_diff
               CInfinitesimal_hcmod_iff hcmod hypreal_diff
               Infinitesimal_FreeUltrafilterNat_iff
+              star_of_def star_n_def
               Infinitesimal_approx_minus [symmetric] hypreal_of_real_def)
-apply (rule bexI, rule_tac [2] lemma_hyprel_refl, safe)
+apply (rule bexI, rule_tac [2] lemma_starrel_refl, safe)
 apply (drule_tac x = u in spec, auto)
 apply (drule_tac x = s in spec, auto, ultra)
 apply (drule sym, auto)
@@ -241,7 +242,7 @@
 apply (drule lemma_crsimp [THEN complex_seq_to_hcomplex_CInfinitesimal])
 apply (simp add: CInfinitesimal_hcmod_iff hcomplex_of_complex_def 
              Infinitesimal_FreeUltrafilterNat_iff hcomplex_diff hcmod)
-apply (auto simp add: hypreal_of_real_def hypreal_diff)
+apply (auto simp add: hypreal_of_real_def star_of_def star_n_def hypreal_diff)
 apply (drule_tac x = r in spec, clarify)
 apply (drule FreeUltrafilterNat_all, ultra)
 done
@@ -427,7 +428,7 @@
 apply (auto simp add: NSCLIM_def NSCRLIM_def)
 apply (auto dest!: spec) 
 apply (rule_tac z = x in eq_Abs_hcomplex)
-apply (simp add: capprox_approx_iff starfunC hcomplex_of_complex_def starfunCR hypreal_of_real_def)
+apply (simp add: capprox_approx_iff starfunC hcomplex_of_complex_def starfunCR hypreal_of_real_def star_of_def star_n_def)
 done
 
 lemma CLIM_CRLIM_Re_Im_iff:
diff -r 17256fe71aca -r ad73fb6144cf src/HOL/Complex/CStar.thy
--- a/src/HOL/Complex/CStar.thy	Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Complex/CStar.thy	Tue Sep 06 23:16:48 2005 +0200
@@ -44,11 +44,11 @@
 
     starfunRC :: "(real => complex) => hypreal => hcomplex"
                  ("*fRc* _" [80] 80)
-    "*fRc* f  == (%x. Abs_hcomplex(\<Union>X \<in> Rep_hypreal(x). hcomplexrel``{%n. f (X n)}))"
+    "*fRc* f  == (%x. Abs_hcomplex(\<Union>X \<in> Rep_star(x). hcomplexrel``{%n. f (X n)}))"
 
     starfunRC_n :: "(nat => (real => complex)) => hypreal => hcomplex"
                    ("*fRcn* _" [80] 80)
-    "*fRcn* F  == (%x. Abs_hcomplex(\<Union>X \<in> Rep_hypreal(x). hcomplexrel``{%n. (F n)(X n)}))"
+    "*fRcn* F  == (%x. Abs_hcomplex(\<Union>X \<in> Rep_star(x). hcomplexrel``{%n. (F n)(X n)}))"
 
     InternalRCFuns :: "(hypreal => hcomplex) set"
     "InternalRCFuns == {X. \<exists>F. X = *fRcn* F}"
@@ -57,11 +57,11 @@
 
     starfunCR :: "(complex => real) => hcomplex => hypreal"
                  ("*fcR* _" [80] 80)
-    "*fcR* f  == (%x. Abs_hypreal(\<Union>X \<in> Rep_hcomplex(x). hyprel``{%n. f (X n)}))"
+    "*fcR* f  == (%x. Abs_star(\<Union>X \<in> Rep_hcomplex(x). starrel``{%n. f (X n)}))"
 
     starfunCR_n :: "(nat => (complex => real)) => hcomplex => hypreal"
                    ("*fcRn* _" [80] 80)
-    "*fcRn* F  == (%x. Abs_hypreal(\<Union>X \<in> Rep_hcomplex(x). hyprel``{%n. (F n)(X n)}))"
+    "*fcRn* F  == (%x. Abs_star(\<Union>X \<in> Rep_hcomplex(x). starrel``{%n. (F n)(X n)}))"
 
     InternalCRFuns :: "(hcomplex => hypreal) set"
     "InternalCRFuns == {X. \<exists>F. X = *fcRn* F}"
@@ -227,7 +227,7 @@
 done
 
 lemma starfunRC:
-      "( *fRc* f) (Abs_hypreal(hyprel``{%n. X n})) =
+      "( *fRc* f) (Abs_star(starrel``{%n. X n})) =
        Abs_hcomplex(hcomplexrel `` {%n. f (X n)})"
 apply (simp add: starfunRC_def)
 apply (rule arg_cong [where f = Abs_hcomplex], auto, ultra)
@@ -235,9 +235,9 @@
 
 lemma starfunCR:
       "( *fcR* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) =
-       Abs_hypreal(hyprel `` {%n. f (X n)})"
+       Abs_star(starrel `` {%n. f (X n)})"
 apply (simp add: starfunCR_def)
-apply (rule arg_cong [where f = Abs_hypreal])
+apply (rule arg_cong [where f = Abs_star])
 apply (auto iff add: hcomplexrel_iff, ultra)
 done
 
@@ -251,7 +251,7 @@
 
 lemma starfunRC_mult:
     "( *fRc* f) z * ( *fRc* g) z = ( *fRc* (%x. f x * g x)) z"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
 apply (simp add: starfunRC hcomplex_mult)
 done
 declare starfunRC_mult [symmetric, simp]
@@ -272,7 +272,7 @@
 declare starfunC_add [symmetric, simp]
 
 lemma starfunRC_add: "( *fRc* f) z + ( *fRc* g) z = ( *fRc* (%x. f x + g x)) z"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
 apply (simp add: starfunRC hcomplex_add)
 done
 declare starfunRC_add [symmetric, simp]
@@ -290,7 +290,7 @@
 done
 
 lemma starfunRC_minus [simp]: "( *fRc* (%x. - f x)) x = - ( *fRc* f) x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
 apply (simp add: starfunRC hcomplex_minus)
 done
 
@@ -329,7 +329,7 @@
 lemma starfunC_starfunRC_o2:
     "(%x. ( *fc* f) (( *fRc* g) x)) = *fRc* (%x. f (g x))"
 apply (rule ext)
-apply (rule_tac z = x in eq_Abs_hypreal)
+apply (rule_tac z = x in eq_Abs_star)
 apply (simp add: starfunRC starfunC)
 done
 
@@ -352,13 +352,13 @@
 done
 
 lemma starfunRC_const_fun [simp]: "( *fRc* (%x. k)) z = hcomplex_of_complex k"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
 apply (simp add: starfunRC hcomplex_of_complex_def)
 done
 
 lemma starfunCR_const_fun [simp]: "( *fcR* (%x. k)) z = hypreal_of_real k"
 apply (cases z)
-apply (simp add: starfunCR hypreal_of_real_def)
+apply (simp add: starfunCR hypreal_of_real_def star_of_def star_n_def)
 done
 
 lemma starfunC_inverse: "inverse (( *fc* f) x) = ( *fc* (%x. inverse (f x))) x"
@@ -369,7 +369,7 @@
 
 lemma starfunRC_inverse:
     "inverse (( *fRc* f) x) = ( *fRc* (%x. inverse (f x))) x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
 apply (simp add: starfunRC hcomplex_inverse)
 done
 declare starfunRC_inverse [symmetric, simp]
@@ -387,11 +387,11 @@
 
 lemma starfunRC_eq [simp]:
     "( *fRc* f) (hypreal_of_real a) = hcomplex_of_complex (f a)"
-by (simp add: starfunRC hcomplex_of_complex_def hypreal_of_real_def)
+by (simp add: starfunRC hcomplex_of_complex_def hypreal_of_real_def star_of_def star_n_def)
 
 lemma starfunCR_eq [simp]:
     "( *fcR* f) (hcomplex_of_complex a) = hypreal_of_real (f a)"
-by (simp add: starfunCR hcomplex_of_complex_def hypreal_of_real_def)
+by (simp add: starfunCR hcomplex_of_complex_def hypreal_of_real_def star_of_def star_n_def)
 
 lemma starfunC_capprox:
     "( *fc* f) (hcomplex_of_complex a) @c= hcomplex_of_complex (f a)"
@@ -428,8 +428,8 @@
 
 lemma starfunRC_lambda_cancel:
     "( *fRc* (%h. f (x + h))) y  = ( *fRc* f) (hypreal_of_real x + y)"
-apply (cases y)
-apply (simp add: starfunRC hypreal_of_real_def hypreal_add)
+apply (rule_tac z=y in eq_Abs_star)
+apply (simp add: starfunRC hypreal_of_real_def star_of_def star_n_def hypreal_add)
 done
 
 lemma starfunC_lambda_cancel2:
@@ -446,8 +446,8 @@
 
 lemma starfunRC_lambda_cancel2:
     "( *fRc* (%h. f(g(x + h)))) y = ( *fRc* (f o g)) (hypreal_of_real x + y)"
-apply (cases y)
-apply (simp add: starfunRC hypreal_of_real_def hypreal_add)
+apply (rule_tac z=y in eq_Abs_star)
+apply (simp add: starfunRC hypreal_of_real_def star_of_def star_n_def hypreal_add)
 done
 
 lemma starfunC_mult_CFinite_capprox:
diff -r 17256fe71aca -r ad73fb6144cf src/HOL/Complex/NSCA.thy
--- a/src/HOL/Complex/NSCA.thy	Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Complex/NSCA.thy	Tue Sep 06 23:16:48 2005 +0200
@@ -80,7 +80,7 @@
 
 lemma SReal_hcmod_hcomplex_of_complex [simp]:
      "hcmod (hcomplex_of_complex r) \<in> Reals"
-by (simp add: hcomplex_of_complex_def hcmod SReal_def hypreal_of_real_def)
+by (simp add: hcomplex_of_complex_def hcmod SReal_def hypreal_of_real_def star_of_def star_n_def)
 
 lemma SReal_hcmod_number_of [simp]: "hcmod (number_of w ::hcomplex) \<in> Reals"
 apply (subst hcomplex_number_of [symmetric])
@@ -135,7 +135,7 @@
       "z \<in> SComplex ==> hcmod z \<in> Reals"
 apply (simp add: SComplex_def SReal_def)
 apply (rule_tac z = z in eq_Abs_hcomplex)
-apply (auto simp add: hcmod hypreal_of_real_def hcomplex_of_complex_def cmod_def)
+apply (auto simp add: hcmod hypreal_of_real_def star_of_def star_n_def hcomplex_of_complex_def cmod_def)
 apply (rule_tac x = "cmod r" in exI)
 apply (simp add: cmod_def, ultra)
 done
@@ -660,8 +660,8 @@
 
 lemma hcomplex_capproxD1:
      "Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n})  
-      ==> Abs_hypreal(hyprel `` {%n. Re(X n)}) @=  
-          Abs_hypreal(hyprel `` {%n. Re(Y n)})"
+      ==> Abs_star(starrel `` {%n. Re(X n)}) @=  
+          Abs_star(starrel `` {%n. Re(Y n)})"
 apply (auto simp add: approx_FreeUltrafilterNat_iff)
 apply (drule capprox_minus_iff [THEN iffD1])
 apply (auto simp add: hcomplex_minus hcomplex_add mem_cinfmal_iff [symmetric] CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2)
@@ -679,8 +679,8 @@
 (* same proof *)
 lemma hcomplex_capproxD2:
      "Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n})  
-      ==> Abs_hypreal(hyprel `` {%n. Im(X n)}) @=  
-          Abs_hypreal(hyprel `` {%n. Im(Y n)})"
+      ==> Abs_star(starrel `` {%n. Im(X n)}) @=  
+          Abs_star(starrel `` {%n. Im(Y n)})"
 apply (auto simp add: approx_FreeUltrafilterNat_iff)
 apply (drule capprox_minus_iff [THEN iffD1])
 apply (auto simp add: hcomplex_minus hcomplex_add mem_cinfmal_iff [symmetric] CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2)
@@ -695,16 +695,16 @@
 done
 
 lemma hcomplex_capproxI:
-     "[| Abs_hypreal(hyprel `` {%n. Re(X n)}) @=  
-         Abs_hypreal(hyprel `` {%n. Re(Y n)});  
-         Abs_hypreal(hyprel `` {%n. Im(X n)}) @=  
-         Abs_hypreal(hyprel `` {%n. Im(Y n)})  
+     "[| Abs_star(starrel `` {%n. Re(X n)}) @=  
+         Abs_star(starrel `` {%n. Re(Y n)});  
+         Abs_star(starrel `` {%n. Im(X n)}) @=  
+         Abs_star(starrel `` {%n. Im(Y n)})  
       |] ==> Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n})"
 apply (drule approx_minus_iff [THEN iffD1])
 apply (drule approx_minus_iff [THEN iffD1])
 apply (rule capprox_minus_iff [THEN iffD2])
 apply (auto simp add: mem_cinfmal_iff [symmetric] mem_infmal_iff [symmetric] hypreal_minus hypreal_add hcomplex_minus hcomplex_add CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff)
-apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
+apply (rule bexI, rule_tac [2] lemma_starrel_refl, auto)
 apply (drule_tac x = "u/2" in spec)
 apply (drule_tac x = "u/2" in spec, auto, ultra)
 apply (drule sym, drule sym)
@@ -719,22 +719,22 @@
 
 lemma capprox_approx_iff:
      "(Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n})) = 
-       (Abs_hypreal(hyprel `` {%n. Re(X n)}) @= Abs_hypreal(hyprel `` {%n. Re(Y n)}) &  
-        Abs_hypreal(hyprel `` {%n. Im(X n)}) @= Abs_hypreal(hyprel `` {%n. Im(Y n)}))"
+       (Abs_star(starrel `` {%n. Re(X n)}) @= Abs_star(starrel `` {%n. Re(Y n)}) &  
+        Abs_star(starrel `` {%n. Im(X n)}) @= Abs_star(starrel `` {%n. Im(Y n)}))"
 apply (blast intro: hcomplex_capproxI hcomplex_capproxD1 hcomplex_capproxD2)
 done
 
 lemma hcomplex_of_hypreal_capprox_iff [simp]:
      "(hcomplex_of_hypreal x @c= hcomplex_of_hypreal z) = (x @= z)"
-apply (cases x, cases z)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=z in eq_Abs_star)
 apply (simp add: hcomplex_of_hypreal capprox_approx_iff)
 done
 
 lemma CFinite_HFinite_Re:
      "Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> CFinite  
-      ==> Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> HFinite"
+      ==> Abs_star(starrel `` {%n. Re(X n)}) \<in> HFinite"
 apply (auto simp add: CFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff)
-apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
+apply (rule bexI, rule_tac [2] lemma_starrel_refl)
 apply (rule_tac x = u in exI, ultra)
 apply (drule sym, case_tac "X x")
 apply (auto simp add: complex_mod numeral_2_eq_2 simp del: realpow_Suc)
@@ -746,9 +746,9 @@
 
 lemma CFinite_HFinite_Im:
      "Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> CFinite  
-      ==> Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> HFinite"
+      ==> Abs_star(starrel `` {%n. Im(X n)}) \<in> HFinite"
 apply (auto simp add: CFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff)
-apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
+apply (rule bexI, rule_tac [2] lemma_starrel_refl)
 apply (rule_tac x = u in exI, ultra)
 apply (drule sym, case_tac "X x")
 apply (auto simp add: complex_mod simp del: realpow_Suc)
@@ -758,12 +758,12 @@
 done
 
 lemma HFinite_Re_Im_CFinite:
-     "[| Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> HFinite;  
-         Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> HFinite  
+     "[| Abs_star(starrel `` {%n. Re(X n)}) \<in> HFinite;  
+         Abs_star(starrel `` {%n. Im(X n)}) \<in> HFinite  
       |] ==> Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> CFinite"
 apply (auto simp add: CFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff)
 apply (rename_tac Y Z u v)
-apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
+apply (rule bexI, rule_tac [2] lemma_starrel_refl)
 apply (rule_tac x = "2* (u + v) " in exI)
 apply ultra
 apply (drule sym, case_tac "X x")
@@ -779,42 +779,42 @@
 
 lemma CFinite_HFinite_iff:
      "(Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> CFinite) =  
-      (Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> HFinite &  
-       Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> HFinite)"
+      (Abs_star(starrel `` {%n. Re(X n)}) \<in> HFinite &  
+       Abs_star(starrel `` {%n. Im(X n)}) \<in> HFinite)"
 by (blast intro: HFinite_Re_Im_CFinite CFinite_HFinite_Im CFinite_HFinite_Re)
 
 lemma SComplex_Re_SReal:
      "Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> SComplex  
-      ==> Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> Reals"
-apply (auto simp add: SComplex_def hcomplex_of_complex_def SReal_def hypreal_of_real_def)
+      ==> Abs_star(starrel `` {%n. Re(X n)}) \<in> Reals"
+apply (auto simp add: SComplex_def hcomplex_of_complex_def SReal_def hypreal_of_real_def star_of_def star_n_def)
 apply (rule_tac x = "Re r" in exI, ultra)
 done
 
 lemma SComplex_Im_SReal:
      "Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> SComplex  
-      ==> Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> Reals"
-apply (auto simp add: SComplex_def hcomplex_of_complex_def SReal_def hypreal_of_real_def)
+      ==> Abs_star(starrel `` {%n. Im(X n)}) \<in> Reals"
+apply (auto simp add: SComplex_def hcomplex_of_complex_def SReal_def hypreal_of_real_def star_of_def star_n_def)
 apply (rule_tac x = "Im r" in exI, ultra)
 done
 
 lemma Reals_Re_Im_SComplex:
-     "[| Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> Reals;  
-         Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> Reals  
+     "[| Abs_star(starrel `` {%n. Re(X n)}) \<in> Reals;  
+         Abs_star(starrel `` {%n. Im(X n)}) \<in> Reals  
       |] ==> Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> SComplex"
-apply (auto simp add: SComplex_def hcomplex_of_complex_def SReal_def hypreal_of_real_def)
+apply (auto simp add: SComplex_def hcomplex_of_complex_def SReal_def hypreal_of_real_def star_of_def star_n_def)
 apply (rule_tac x = "Complex r ra" in exI, ultra)
 done
 
 lemma SComplex_SReal_iff:
      "(Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> SComplex) =  
-      (Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> Reals &  
-       Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> Reals)"
+      (Abs_star(starrel `` {%n. Re(X n)}) \<in> Reals &  
+       Abs_star(starrel `` {%n. Im(X n)}) \<in> Reals)"
 by (blast intro: SComplex_Re_SReal SComplex_Im_SReal Reals_Re_Im_SComplex)
 
 lemma CInfinitesimal_Infinitesimal_iff:
      "(Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> CInfinitesimal) =  
-      (Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> Infinitesimal &  
-       Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> Infinitesimal)"
+      (Abs_star(starrel `` {%n. Re(X n)}) \<in> Infinitesimal &  
+       Abs_star(starrel `` {%n. Im(X n)}) \<in> Infinitesimal)"
 by (simp add: mem_cinfmal_iff mem_infmal_iff hcomplex_zero_num hypreal_zero_num capprox_approx_iff)
 
 lemma eq_Abs_hcomplex_EX:
@@ -835,8 +835,8 @@
 apply (rule_tac z = x in eq_Abs_hcomplex)
 apply (auto simp add: CFinite_HFinite_iff eq_Abs_hcomplex_Bex SComplex_SReal_iff capprox_approx_iff)
 apply (drule st_part_Ex, safe)+
-apply (rule_tac z = t in eq_Abs_hypreal)
-apply (rule_tac z = ta in eq_Abs_hypreal, auto)
+apply (rule_tac z = t in eq_Abs_star)
+apply (rule_tac z = ta in eq_Abs_star, auto)
 apply (rule_tac x = "%n. Complex (xa n) (xb n) " in exI)
 apply auto
 done
@@ -1135,13 +1135,13 @@
 
 lemma CFinite_HFinite_hcomplex_of_hypreal:
      "z \<in> HFinite ==> hcomplex_of_hypreal z \<in> CFinite"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
 apply (simp add: hcomplex_of_hypreal CFinite_HFinite_iff hypreal_zero_def [symmetric])
 done
 
 lemma SComplex_SReal_hcomplex_of_hypreal:
      "x \<in> Reals ==>  hcomplex_of_hypreal x \<in> SComplex"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
 apply (simp add: hcomplex_of_hypreal SComplex_SReal_iff hypreal_zero_def [symmetric])
 done
 
@@ -1172,36 +1172,36 @@
 
 lemma CInfinite_HInfinite_iff:
      "(Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> CInfinite) =  
-      (Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> HInfinite |  
-       Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> HInfinite)"
+      (Abs_star(starrel `` {%n. Re(X n)}) \<in> HInfinite |  
+       Abs_star(starrel `` {%n. Im(X n)}) \<in> HInfinite)"
 by (simp add: CInfinite_CFinite_iff HInfinite_HFinite_iff CFinite_HFinite_iff)
 
 text{*These theorems should probably be deleted*}
 lemma hcomplex_split_CInfinitesimal_iff:
      "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> CInfinitesimal) =  
       (x \<in> Infinitesimal & y \<in> Infinitesimal)"
-apply (cases x, cases y)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
 apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal CInfinitesimal_Infinitesimal_iff)
 done
 
 lemma hcomplex_split_CFinite_iff:
      "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> CFinite) =  
       (x \<in> HFinite & y \<in> HFinite)"
-apply (cases x, cases y)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
 apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal CFinite_HFinite_iff)
 done
 
 lemma hcomplex_split_SComplex_iff:
      "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> SComplex) =  
       (x \<in> Reals & y \<in> Reals)"
-apply (cases x, cases y)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
 apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal SComplex_SReal_iff)
 done
 
 lemma hcomplex_split_CInfinite_iff:
      "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> CInfinite) =  
       (x \<in> HInfinite | y \<in> HInfinite)"
-apply (cases x, cases y)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
 apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal CInfinite_HInfinite_iff)
 done
 
@@ -1209,7 +1209,8 @@
      "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y @c=  
        hcomplex_of_hypreal x' + iii * hcomplex_of_hypreal y') =  
       (x @= x' & y @= y')"
-apply (cases x, cases y, cases x', cases y')
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
+apply (rule_tac z=x' in eq_Abs_star, rule_tac z=y' in eq_Abs_star)
 apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal capprox_approx_iff)
 done
 
diff -r 17256fe71aca -r ad73fb6144cf src/HOL/Complex/NSComplex.thy
--- a/src/HOL/Complex/NSComplex.thy	Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Complex/NSComplex.thy	Tue Sep 06 23:16:48 2005 +0200
@@ -48,17 +48,17 @@
   (*--- real and Imaginary parts ---*)
 
   hRe :: "hcomplex => hypreal"
-  "hRe(z) == Abs_hypreal(UN X:Rep_hcomplex(z). hyprel `` {%n. Re (X n)})"
+  "hRe(z) == Abs_star(UN X:Rep_hcomplex(z). starrel `` {%n. Re (X n)})"
 
   hIm :: "hcomplex => hypreal"
-  "hIm(z) == Abs_hypreal(UN X:Rep_hcomplex(z). hyprel `` {%n. Im (X n)})"
+  "hIm(z) == Abs_star(UN X:Rep_hcomplex(z). starrel `` {%n. Im (X n)})"
 
 
   (*----------- modulus ------------*)
 
   hcmod :: "hcomplex => hypreal"
-  "hcmod z == Abs_hypreal(UN X: Rep_hcomplex(z).
-			  hyprel `` {%n. cmod (X n)})"
+  "hcmod z == Abs_star(UN X: Rep_hcomplex(z).
+			  starrel `` {%n. cmod (X n)})"
 
   (*------ imaginary unit ----------*)
 
@@ -76,16 +76,16 @@
   "hsgn z == Abs_hcomplex(UN X:Rep_hcomplex(z). hcomplexrel `` {%n. sgn(X n)})"
 
   harg :: "hcomplex => hypreal"
-  "harg z == Abs_hypreal(UN X:Rep_hcomplex(z). hyprel `` {%n. arg(X n)})"
+  "harg z == Abs_star(UN X:Rep_hcomplex(z). starrel `` {%n. arg(X n)})"
 
   (* abbreviation for (cos a + i sin a) *)
   hcis :: "hypreal => hcomplex"
-  "hcis a == Abs_hcomplex(UN X:Rep_hypreal(a). hcomplexrel `` {%n. cis (X n)})"
+  "hcis a == Abs_hcomplex(UN X:Rep_star(a). hcomplexrel `` {%n. cis (X n)})"
 
   (*----- injection from hyperreals -----*)
 
   hcomplex_of_hypreal :: "hypreal => hcomplex"
-  "hcomplex_of_hypreal r == Abs_hcomplex(UN X:Rep_hypreal(r).
+  "hcomplex_of_hypreal r == Abs_hcomplex(UN X:Rep_star(r).
 			       hcomplexrel `` {%n. complex_of_real (X n)})"
 
   (* abbreviation for r*(cos a + i sin a) *)
@@ -186,17 +186,17 @@
 
 lemma hRe:
      "hRe(Abs_hcomplex (hcomplexrel `` {X})) =
-      Abs_hypreal(hyprel `` {%n. Re(X n)})"
+      Abs_star(starrel `` {%n. Re(X n)})"
 apply (simp add: hRe_def)
-apply (rule_tac f = Abs_hypreal in arg_cong)
+apply (rule_tac f = Abs_star in arg_cong)
 apply (auto iff: hcomplexrel_iff, ultra)
 done
 
 lemma hIm:
      "hIm(Abs_hcomplex (hcomplexrel `` {X})) =
-      Abs_hypreal(hyprel `` {%n. Im(X n)})"
+      Abs_star(starrel `` {%n. Im(X n)})"
 apply (simp add: hIm_def)
-apply (rule_tac f = Abs_hypreal in arg_cong)
+apply (rule_tac f = Abs_star in arg_cong)
 apply (auto iff: hcomplexrel_iff, ultra)
 done
 
@@ -452,7 +452,7 @@
 subsection{*Embedding Properties for @{term hcomplex_of_hypreal} Map*}
 
 lemma hcomplex_of_hypreal:
-  "hcomplex_of_hypreal (Abs_hypreal(hyprel `` {%n. X n})) =
+  "hcomplex_of_hypreal (Abs_star(starrel `` {%n. X n})) =
       Abs_hcomplex(hcomplexrel `` {%n. complex_of_real (X n)})"
 apply (simp add: hcomplex_of_hypreal_def)
 apply (rule_tac f = Abs_hcomplex in arg_cong, auto iff: hcomplexrel_iff, ultra)
@@ -460,7 +460,7 @@
 
 lemma hcomplex_of_hypreal_cancel_iff [iff]:
      "(hcomplex_of_hypreal x = hcomplex_of_hypreal y) = (x = y)"
-apply (cases x, cases y)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
 apply (simp add: hcomplex_of_hypreal)
 done
 
@@ -472,19 +472,19 @@
 
 lemma hcomplex_of_hypreal_minus [simp]:
      "hcomplex_of_hypreal(-x) = - hcomplex_of_hypreal x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
 apply (simp add: hcomplex_of_hypreal hcomplex_minus hypreal_minus)
 done
 
 lemma hcomplex_of_hypreal_inverse [simp]:
      "hcomplex_of_hypreal(inverse x) = inverse(hcomplex_of_hypreal x)"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
 apply (simp add: hcomplex_of_hypreal hypreal_inverse hcomplex_inverse)
 done
 
 lemma hcomplex_of_hypreal_add [simp]:
   "hcomplex_of_hypreal (x + y) = hcomplex_of_hypreal x + hcomplex_of_hypreal y"
-apply (cases x, cases y)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
 apply (simp add: hcomplex_of_hypreal hypreal_add hcomplex_add)
 done
 
@@ -495,7 +495,7 @@
 
 lemma hcomplex_of_hypreal_mult [simp]:
   "hcomplex_of_hypreal (x * y) = hcomplex_of_hypreal x * hcomplex_of_hypreal y"
-apply (cases x, cases y)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
 apply (simp add: hcomplex_of_hypreal hypreal_mult hcomplex_mult)
 done
 
@@ -507,35 +507,35 @@
 done
 
 lemma hRe_hcomplex_of_hypreal [simp]: "hRe(hcomplex_of_hypreal z) = z"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
 apply (auto simp add: hcomplex_of_hypreal hRe)
 done
 
 lemma hIm_hcomplex_of_hypreal [simp]: "hIm(hcomplex_of_hypreal z) = 0"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
 apply (auto simp add: hcomplex_of_hypreal hIm hypreal_zero_num)
 done
 
 lemma hcomplex_of_hypreal_epsilon_not_zero [simp]:
      "hcomplex_of_hypreal epsilon \<noteq> 0"
-by (auto simp add: hcomplex_of_hypreal epsilon_def hcomplex_zero_def)
+by (auto simp add: hcomplex_of_hypreal epsilon_def star_n_def hcomplex_zero_def)
 
 
 subsection{*HComplex theorems*}
 
 lemma hRe_HComplex [simp]: "hRe (HComplex x y) = x"
-apply (cases x, cases y)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
 apply (simp add: HComplex_def hRe iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
 done
 
 lemma hIm_HComplex [simp]: "hIm (HComplex x y) = y"
-apply (cases x, cases y)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
 apply (simp add: HComplex_def hIm iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
 done
 
 text{*Relates the two nonstandard constructions*}
 lemma HComplex_eq_Abs_hcomplex_Complex:
-     "HComplex (Abs_hypreal (hyprel `` {X})) (Abs_hypreal (hyprel `` {Y})) =
+     "HComplex (Abs_star (starrel `` {X})) (Abs_star (starrel `` {Y})) =
       Abs_hcomplex(hcomplexrel `` {%n::nat. Complex (X n) (Y n)})";
 by (simp add: hcomplex_hRe_hIm_cancel_iff hRe hIm) 
 
@@ -551,10 +551,10 @@
 
 lemma hcmod:
   "hcmod (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
-      Abs_hypreal(hyprel `` {%n. cmod (X n)})"
+      Abs_star(starrel `` {%n. cmod (X n)})"
 
 apply (simp add: hcmod_def)
-apply (rule_tac f = Abs_hypreal in arg_cong)
+apply (rule_tac f = Abs_star in arg_cong)
 apply (auto iff: hcomplexrel_iff, ultra)
 done
 
@@ -565,7 +565,7 @@
 by (simp add: hcomplex_one_def hcmod hypreal_one_num)
 
 lemma hcmod_hcomplex_of_hypreal [simp]: "hcmod(hcomplex_of_hypreal x) = abs x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
 apply (auto simp add: hcmod hcomplex_of_hypreal hypreal_hrabs)
 done
 
@@ -578,7 +578,8 @@
 apply (rule iffI) 
  prefer 2 apply simp 
 apply (simp add: HComplex_def iii_def) 
-apply (cases x, cases y, cases x', cases y')
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star,
+       rule_tac z=x' in eq_Abs_star, rule_tac z=y' in eq_Abs_star)
 apply (auto simp add: iii_def hcomplex_mult hcomplex_add hcomplex_of_hypreal)
 apply (ultra+) 
 done
@@ -651,7 +652,7 @@
 
 lemma hcomplex_hcnj_hcomplex_of_hypreal [simp]:
      "hcnj (hcomplex_of_hypreal x) = hcomplex_of_hypreal x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
 apply (simp add: hcnj hcomplex_of_hypreal)
 done
 
@@ -755,6 +756,7 @@
                   del: realpow_Suc)
 apply (simp add: numeral_2_eq_2 [symmetric] complex_mod_add_squared_eq
                  hypreal_add [symmetric] hypreal_mult [symmetric]
+                 star_n_def [symmetric] star_of_def [symmetric]
                  hypreal_of_real_def [symmetric])
 done
 
@@ -793,14 +795,14 @@
 
 lemma hcmod_add_less:
      "[| hcmod x < r; hcmod y < s |] ==> hcmod (x + y) < r + s"
-apply (cases x, cases y, cases r, cases s)
+apply (cases x, cases y, rule_tac z=r in eq_Abs_star, rule_tac z=s in eq_Abs_star)
 apply (simp add: hcmod hcomplex_add hypreal_add hypreal_less, ultra)
 apply (auto intro: complex_mod_add_less)
 done
 
 lemma hcmod_mult_less:
      "[| hcmod x < r; hcmod y < s |] ==> hcmod (x * y) < r * s"
-apply (cases x, cases y, cases r, cases s)
+apply (cases x, cases y, rule_tac z=r in eq_Abs_star, rule_tac z=s in eq_Abs_star)
 apply (simp add: hcmod hypreal_mult hypreal_less hcomplex_mult, ultra)
 apply (auto intro: complex_mod_mult_less)
 done
@@ -824,7 +826,7 @@
 
 lemma hcomplex_of_hypreal_hyperpow:
      "hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) hcpow n"
-apply (cases x, cases n)
+apply (rule_tac z=x in eq_Abs_star, cases n)
 apply (simp add: hcomplex_of_hypreal hyperpow hcpow complex_of_real_pow)
 done
 
@@ -942,7 +944,7 @@
 
 
 lemma hcmod_i: "hcmod (HComplex x y) = ( *f* sqrt) (x ^ 2 + y ^ 2)"
-apply (cases x, cases y) 
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star) 
 apply (simp add: HComplex_eq_Abs_hcomplex_Complex starfun 
                  hypreal_mult hypreal_add hcmod numeral_2_eq_2)
 done
@@ -985,7 +987,7 @@
      "inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) =
       hcomplex_of_hypreal(x/(x ^ 2 + y ^ 2)) -
       iii * hcomplex_of_hypreal(y/(x ^ 2 + y ^ 2))"
-apply (cases x, cases y)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
 apply (simp add: hcomplex_of_hypreal hcomplex_mult hcomplex_add iii_def
          starfun hypreal_mult hypreal_add hcomplex_inverse hypreal_divide
          hcomplex_diff numeral_2_eq_2 complex_of_real_def i_def)
@@ -1001,18 +1003,18 @@
 
 lemma hRe_mult_i_eq[simp]:
     "hRe (iii * hcomplex_of_hypreal y) = 0"
-apply (simp add: iii_def, cases y)
+apply (simp add: iii_def, rule_tac z=y in eq_Abs_star)
 apply (simp add: hcomplex_of_hypreal hcomplex_mult hRe hypreal_zero_num)
 done
 
 lemma hIm_mult_i_eq [simp]:
     "hIm (iii * hcomplex_of_hypreal y) = y"
-apply (simp add: iii_def, cases y)
+apply (simp add: iii_def, rule_tac z=y in eq_Abs_star)
 apply (simp add: hcomplex_of_hypreal hcomplex_mult hIm hypreal_zero_num)
 done
 
 lemma hcmod_mult_i [simp]: "hcmod (iii * hcomplex_of_hypreal y) = abs y"
-apply (cases y)
+apply (rule_tac z=y in eq_Abs_star)
 apply (simp add: hcomplex_of_hypreal hcmod hypreal_hrabs iii_def hcomplex_mult)
 done
 
@@ -1025,22 +1027,22 @@
 
 lemma harg:
   "harg (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
-      Abs_hypreal(hyprel `` {%n. arg (X n)})"
+      Abs_star(starrel `` {%n. arg (X n)})"
 apply (simp add: harg_def)
-apply (rule_tac f = Abs_hypreal in arg_cong)
+apply (rule_tac f = Abs_star in arg_cong)
 apply (auto iff: hcomplexrel_iff, ultra)
 done
 
 lemma cos_harg_i_mult_zero_pos:
      "0 < y ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
-apply (cases y)
+apply (rule_tac z=y in eq_Abs_star)
 apply (simp add: HComplex_def hcomplex_of_hypreal iii_def hcomplex_mult
                 hcomplex_add hypreal_zero_num hypreal_less starfun harg, ultra)
 done
 
 lemma cos_harg_i_mult_zero_neg:
      "y < 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
-apply (cases y)
+apply (rule_tac z=y in eq_Abs_star)
 apply (simp add: HComplex_def hcomplex_of_hypreal iii_def hcomplex_mult
                  hcomplex_add hypreal_zero_num hypreal_less starfun harg, ultra)
 done
@@ -1052,7 +1054,7 @@
 
 lemma hcomplex_of_hypreal_zero_iff [simp]:
      "(hcomplex_of_hypreal y = 0) = (y = 0)"
-apply (cases y)
+apply (rule_tac z=y in eq_Abs_star)
 apply (simp add: hcomplex_of_hypreal hypreal_zero_num hcomplex_zero_def)
 done
 
@@ -1065,10 +1067,10 @@
 
 lemma lemma_hypreal_P_EX2:
      "(\<exists>(x::hypreal) y. P x y) =
-      (\<exists>f g. P (Abs_hypreal(hyprel `` {f})) (Abs_hypreal(hyprel `` {g})))"
+      (\<exists>f g. P (Abs_star(starrel `` {f})) (Abs_star(starrel `` {g})))"
 apply auto
-apply (rule_tac z = x in eq_Abs_hypreal)
-apply (rule_tac z = y in eq_Abs_hypreal, auto)
+apply (rule_tac z = x in eq_Abs_star)
+apply (rule_tac z = y in eq_Abs_star, auto)
 done
 
 lemma hcomplex_split_polar:
@@ -1082,7 +1084,7 @@
 done
 
 lemma hcis:
-  "hcis (Abs_hypreal(hyprel `` {%n. X n})) =
+  "hcis (Abs_star(starrel `` {%n. X n})) =
       Abs_hcomplex(hcomplexrel `` {%n. cis (X n)})"
 apply (simp add: hcis_def)
 apply (rule_tac f = Abs_hcomplex in arg_cong, auto iff: hcomplexrel_iff, ultra)
@@ -1092,12 +1094,12 @@
    "hcis a =
     (hcomplex_of_hypreal(( *f* cos) a) +
     iii * hcomplex_of_hypreal(( *f* sin) a))"
-apply (cases a)
+apply (rule_tac z=a in eq_Abs_star)
 apply (simp add: starfun hcis hcomplex_of_hypreal iii_def hcomplex_mult hcomplex_add cis_def)
 done
 
 lemma hrcis:
-  "hrcis (Abs_hypreal(hyprel `` {%n. X n})) (Abs_hypreal(hyprel `` {%n. Y n})) =
+  "hrcis (Abs_star(starrel `` {%n. X n})) (Abs_star(starrel `` {%n. Y n})) =
       Abs_hcomplex(hcomplexrel `` {%n. rcis (X n) (Y n)})"
 by (simp add: hrcis_def hcomplex_of_hypreal hcomplex_mult hcis rcis_def)
 
@@ -1125,7 +1127,7 @@
 
 lemma hcmod_unit_one [simp]:
      "hcmod (HComplex (( *f* cos) a) (( *f* sin) a)) = 1"
-apply (cases a) 
+apply (rule_tac z=a in eq_Abs_star) 
 apply (simp add: HComplex_def iii_def starfun hcomplex_of_hypreal 
                  hcomplex_mult hcmod hcomplex_add hypreal_one_def)
 done
@@ -1149,13 +1151,13 @@
 
 lemma hrcis_mult:
   "hrcis r1 a * hrcis r2 b = hrcis (r1*r2) (a + b)"
-apply (simp add: hrcis_def, cases r1, cases r2, cases a, cases b)
+apply (simp add: hrcis_def, rule_tac z=r1 in eq_Abs_star, rule_tac z=r2 in eq_Abs_star, rule_tac z=a in eq_Abs_star, rule_tac z=b in eq_Abs_star)
 apply (simp add: hrcis hcis hypreal_add hypreal_mult hcomplex_of_hypreal
                       hcomplex_mult cis_mult [symmetric])
 done
 
 lemma hcis_mult: "hcis a * hcis b = hcis (a + b)"
-apply (cases a, cases b)
+apply (rule_tac z=a in eq_Abs_star, rule_tac z=b in eq_Abs_star)
 apply (simp add: hcis hcomplex_mult hypreal_add cis_mult)
 done
 
@@ -1163,12 +1165,12 @@
 by (simp add: hcomplex_one_def hcis hypreal_zero_num)
 
 lemma hrcis_zero_mod [simp]: "hrcis 0 a = 0"
-apply (simp add: hcomplex_zero_def, cases a)
+apply (simp add: hcomplex_zero_def, rule_tac z=a in eq_Abs_star)
 apply (simp add: hrcis hypreal_zero_num)
 done
 
 lemma hrcis_zero_arg [simp]: "hrcis r 0 = hcomplex_of_hypreal r"
-apply (cases r)
+apply (rule_tac z=r in eq_Abs_star)
 apply (simp add: hrcis hypreal_zero_num hcomplex_of_hypreal)
 done
 
@@ -1180,7 +1182,7 @@
 
 lemma hcis_hypreal_of_nat_Suc_mult:
    "hcis (hypreal_of_nat (Suc n) * a) = hcis a * hcis (hypreal_of_nat n * a)"
-apply (cases a)
+apply (rule_tac z=a in eq_Abs_star)
 apply (simp add: hypreal_of_nat hcis hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult)
 done
 
@@ -1192,12 +1194,12 @@
 lemma hcis_hypreal_of_hypnat_Suc_mult:
      "hcis (hypreal_of_hypnat (n + 1) * a) =
       hcis a * hcis (hypreal_of_hypnat n * a)"
-apply (cases a, cases n)
+apply (rule_tac z=a in eq_Abs_star, cases n)
 apply (simp add: hcis hypreal_of_hypnat hypnat_add hypnat_one_def hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult)
 done
 
 lemma NSDeMoivre_ext: "(hcis a) hcpow n = hcis (hypreal_of_hypnat n * a)"
-apply (cases a, cases n)
+apply (rule_tac z=a in eq_Abs_star, cases n)
 apply (simp add: hcis hypreal_of_hypnat hypreal_mult hcpow DeMoivre)
 done
 
@@ -1212,23 +1214,23 @@
 done
 
 lemma hcis_inverse [simp]: "inverse(hcis a) = hcis (-a)"
-apply (cases a)
+apply (rule_tac z=a in eq_Abs_star)
 apply (simp add: hcomplex_inverse hcis hypreal_minus)
 done
 
 lemma hrcis_inverse: "inverse(hrcis r a) = hrcis (inverse r) (-a)"
-apply (cases a, cases r)
+apply (rule_tac z=a in eq_Abs_star, rule_tac z=r in eq_Abs_star)
 apply (simp add: hcomplex_inverse hrcis hypreal_minus hypreal_inverse rcis_inverse, ultra)
 apply (simp add: real_divide_def)
 done
 
 lemma hRe_hcis [simp]: "hRe(hcis a) = ( *f* cos) a"
-apply (cases a)
+apply (rule_tac z=a in eq_Abs_star)
 apply (simp add: hcis starfun hRe)
 done
 
 lemma hIm_hcis [simp]: "hIm(hcis a) = ( *f* sin) a"
-apply (cases a)
+apply (rule_tac z=a in eq_Abs_star)
 apply (simp add: hcis starfun hIm)
 done
 
@@ -1317,15 +1319,15 @@
 
 lemma hRe_hcomplex_of_complex:
    "hRe (hcomplex_of_complex z) = hypreal_of_real (Re z)"
-by (simp add: hcomplex_of_complex_def hypreal_of_real_def hRe)
+by (simp add: hcomplex_of_complex_def hypreal_of_real_def star_of_def star_n_def hRe)
 
 lemma hIm_hcomplex_of_complex:
    "hIm (hcomplex_of_complex z) = hypreal_of_real (Im z)"
-by (simp add: hcomplex_of_complex_def hypreal_of_real_def hIm)
+by (simp add: hcomplex_of_complex_def hypreal_of_real_def star_of_def star_n_def hIm)
 
 lemma hcmod_hcomplex_of_complex:
      "hcmod (hcomplex_of_complex x) = hypreal_of_real (cmod x)"
-by (simp add: hypreal_of_real_def hcomplex_of_complex_def hcmod)
+by (simp add: hypreal_of_real_def star_of_def star_n_def hcomplex_of_complex_def hcmod)
 
 
 subsection{*Numerals and Arithmetic*}
@@ -1365,6 +1367,7 @@
      "hcomplex_of_hypreal (hypreal_of_real x) =  
       hcomplex_of_complex (complex_of_real x)"
 by (simp add: hypreal_of_real_def hcomplex_of_hypreal hcomplex_of_complex_def 
+              star_of_def star_n_def
               complex_of_real_def)
 
 lemma hcomplex_hypreal_number_of: 
diff -r 17256fe71aca -r ad73fb6144cf src/HOL/Hyperreal/HLog.thy
--- a/src/HOL/Hyperreal/HLog.thy	Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Hyperreal/HLog.thy	Tue Sep 06 23:16:48 2005 +0200
@@ -12,7 +12,7 @@
 
 (* should be in NSA.ML *)
 lemma epsilon_ge_zero [simp]: "0 \<le> epsilon"
-by (simp add: epsilon_def hypreal_zero_num hypreal_le)
+by (simp add: epsilon_def star_n_def hypreal_zero_num hypreal_le)
 
 lemma hpfinite_witness: "epsilon : {x. 0 \<le> x & x : HFinite}"
 by auto
@@ -24,29 +24,29 @@
     "x powhr a == ( *f* exp) (a * ( *f* ln) x)"
   
     hlog :: "[hypreal,hypreal] => hypreal"
-    "hlog a x == Abs_hypreal(\<Union>A \<in> Rep_hypreal(a).\<Union>X \<in> Rep_hypreal(x).
-			     hyprel `` {%n. log (A n) (X n)})"
+    "hlog a x == Abs_star(\<Union>A \<in> Rep_star(a).\<Union>X \<in> Rep_star(x).
+			     starrel `` {%n. log (A n) (X n)})"
 
 
 lemma powhr: 
-    "(Abs_hypreal(hyprel `` {X})) powhr (Abs_hypreal(hyprel `` {Y})) =  
-     Abs_hypreal(hyprel `` {%n.  (X n) powr (Y n)})"
+    "(Abs_star(starrel `` {X})) powhr (Abs_star(starrel `` {Y})) =  
+     Abs_star(starrel `` {%n.  (X n) powr (Y n)})"
 by (simp add: powhr_def starfun hypreal_mult powr_def)
 
 lemma powhr_one_eq_one [simp]: "1 powhr a = 1"
-apply (cases a)
+apply (rule_tac z=a in eq_Abs_star)
 apply (simp add: powhr hypreal_one_num)
 done
 
 lemma powhr_mult:
      "[| 0 < x; 0 < y |] ==> (x * y) powhr a = (x powhr a) * (y powhr a)"
-apply (cases x, cases y, cases a)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star, rule_tac z=a in eq_Abs_star)
 apply (simp add: powhr hypreal_zero_num hypreal_mult hypreal_less, ultra)
 apply (simp add: powr_mult) 
 done
 
 lemma powhr_gt_zero [simp]: "0 < x powhr a"
-apply (cases a, cases x)
+apply (rule_tac z=a in eq_Abs_star, rule_tac z=x in eq_Abs_star)
 apply (simp add: hypreal_zero_def powhr hypreal_less hypreal_zero_num)
 done
 
@@ -54,34 +54,34 @@
 by (rule powhr_gt_zero [THEN hypreal_not_refl2, THEN not_sym])
 
 lemma hypreal_divide: 
-     "(Abs_hypreal(hyprel `` {X}))/(Abs_hypreal(hyprel `` {Y})) =  
-      (Abs_hypreal(hyprel `` {%n. (X n)/(Y n)}))"
+     "(Abs_star(starrel `` {X}))/(Abs_star(starrel `` {Y})) =  
+      (Abs_star(starrel `` {%n. (X n::real)/(Y n)}))"
 by (simp add: divide_inverse hypreal_zero_num hypreal_inverse hypreal_mult) 
 
 lemma powhr_divide:
      "[| 0 < x; 0 < y |] ==> (x / y) powhr a = (x powhr a)/(y powhr a)"
-apply (cases x, cases y, cases a)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star, rule_tac z=a in eq_Abs_star)
 apply (simp add: powhr hypreal_divide hypreal_zero_num hypreal_less, ultra)
 apply (simp add: powr_divide)
 done
 
 lemma powhr_add: "x powhr (a + b) = (x powhr a) * (x powhr b)"
-apply (cases x, cases b, cases a)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=b in eq_Abs_star, rule_tac z=a in eq_Abs_star)
 apply (simp add: powhr hypreal_add hypreal_mult powr_add)
 done
 
 lemma powhr_powhr: "(x powhr a) powhr b = x powhr (a * b)"
-apply (cases x, cases b, cases a)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=b in eq_Abs_star, rule_tac z=a in eq_Abs_star)
 apply (simp add: powhr hypreal_mult powr_powr)
 done
 
 lemma powhr_powhr_swap: "(x powhr a) powhr b = (x powhr b) powhr a"
-apply (cases x, cases b, cases a)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=b in eq_Abs_star, rule_tac z=a in eq_Abs_star)
 apply (simp add: powhr powr_powr_swap)
 done
 
 lemma powhr_minus: "x powhr (-a) = inverse (x powhr a)"
-apply (cases x, cases a)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=a in eq_Abs_star)
 apply (simp add: powhr hypreal_minus hypreal_inverse hypreal_less powr_minus)
 done
 
@@ -89,12 +89,12 @@
 by (simp add: divide_inverse powhr_minus)
 
 lemma powhr_less_mono: "[| a < b; 1 < x |] ==> x powhr a < x powhr b"
-apply (cases x, cases a, cases b)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=a in eq_Abs_star, rule_tac z=b in eq_Abs_star)
 apply (simp add: powhr hypreal_one_num hypreal_less, ultra)
 done
 
 lemma powhr_less_cancel: "[| x powhr a < x powhr b; 1 < x |] ==> a < b"
-apply (cases x, cases a, cases b)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=a in eq_Abs_star, rule_tac z=b in eq_Abs_star)
 apply (simp add: powhr hypreal_one_num hypreal_less, ultra)
 done
 
@@ -107,26 +107,26 @@
 by (simp add: linorder_not_less [symmetric])
 
 lemma hlog: 
-     "hlog (Abs_hypreal(hyprel `` {X})) (Abs_hypreal(hyprel `` {Y})) =  
-      Abs_hypreal(hyprel `` {%n. log (X n) (Y n)})"
+     "hlog (Abs_star(starrel `` {X})) (Abs_star(starrel `` {Y})) =  
+      Abs_star(starrel `` {%n. log (X n) (Y n)})"
 apply (simp add: hlog_def)
-apply (rule arg_cong [where f=Abs_hypreal], auto, ultra)
+apply (rule arg_cong [where f=Abs_star], auto, ultra)
 done
 
 lemma hlog_starfun_ln: "( *f* ln) x = hlog (( *f* exp) 1) x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
 apply (simp add: starfun hlog log_ln hypreal_one_num)
 done
 
 lemma powhr_hlog_cancel [simp]:
      "[| 0 < a; a \<noteq> 1; 0 < x |] ==> a powhr (hlog a x) = x"
-apply (cases x, cases a)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=a in eq_Abs_star)
 apply (simp add: hlog powhr hypreal_zero_num hypreal_less hypreal_one_num, ultra)
 done
 
 lemma hlog_powhr_cancel [simp]:
      "[| 0 < a; a \<noteq> 1 |] ==> hlog a (a powhr y) = y"
-apply (cases y, cases a)
+apply (rule_tac z=y in eq_Abs_star, rule_tac z=a in eq_Abs_star)
 apply (simp add: hlog powhr hypreal_zero_num hypreal_less hypreal_one_num, ultra)
 apply (auto intro: log_powr_cancel) 
 done
@@ -134,27 +134,27 @@
 lemma hlog_mult:
      "[| 0 < a; a \<noteq> 1; 0 < x; 0 < y  |]  
       ==> hlog a (x * y) = hlog a x + hlog a y"
-apply (cases x, cases y, cases a)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star, rule_tac z=a in eq_Abs_star)
 apply (simp add: hlog powhr hypreal_zero_num hypreal_one_num hypreal_less hypreal_add hypreal_mult, ultra)
 apply (simp add: log_mult)
 done
 
 lemma hlog_as_starfun:
      "[| 0 < a; a \<noteq> 1 |] ==> hlog a x = ( *f* ln) x / ( *f* ln) a"
-apply (cases x, cases a)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=a in eq_Abs_star)
 apply (simp add: hlog starfun hypreal_zero_num hypreal_one_num hypreal_divide log_def)
 done
 
 lemma hlog_eq_div_starfun_ln_mult_hlog:
      "[| 0 < a; a \<noteq> 1; 0 < b; b \<noteq> 1; 0 < x |]  
       ==> hlog a x = (( *f* ln) b/( *f*ln) a) * hlog b x"
-apply (cases x, cases a, cases b)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=a in eq_Abs_star, rule_tac z=b in eq_Abs_star)
 apply (simp add: hlog starfun hypreal_zero_num hypreal_one_num hypreal_less hypreal_divide hypreal_mult, ultra)
 apply (auto dest: log_eq_div_ln_mult_log) 
 done
 
 lemma powhr_as_starfun: "x powhr a = ( *f* exp) (a * ( *f* ln) x)"
-apply (cases a, cases x)
+apply (rule_tac z=a in eq_Abs_star, rule_tac z=x in eq_Abs_star)
 apply (simp add: powhr starfun hypreal_mult powr_def)
 done
 
@@ -180,12 +180,12 @@
 by (rule hlog_as_starfun, auto)
 
 lemma hlog_one [simp]: "hlog a 1 = 0"
-apply (cases a)
+apply (rule_tac z=a in eq_Abs_star)
 apply (simp add: hypreal_one_num hypreal_zero_num hlog)
 done
 
 lemma hlog_eq_one [simp]: "[| 0 < a; a \<noteq> 1 |] ==> hlog a a = 1"
-apply (cases a)
+apply (rule_tac z=a in eq_Abs_star)
 apply (simp add: hypreal_one_num hypreal_zero_num hlog hypreal_less, ultra)
 apply (auto intro: log_eq_one) 
 done
@@ -202,7 +202,7 @@
 
 lemma hlog_less_cancel_iff [simp]:
      "[| 1 < a; 0 < x; 0 < y |] ==> (hlog a x < hlog a y) = (x < y)"
-apply (cases a, cases x, cases y)
+apply (rule_tac z=a in eq_Abs_star, rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
 apply (auto simp add: hlog hypreal_less hypreal_zero_num hypreal_one_num, ultra+)
 done
 
diff -r 17256fe71aca -r ad73fb6144cf src/HOL/Hyperreal/HSeries.thy
--- a/src/HOL/Hyperreal/HSeries.thy	Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Hyperreal/HSeries.thy	Tue Sep 06 23:16:48 2005 +0200
@@ -14,8 +14,8 @@
 constdefs 
   sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal"
    "sumhr p == 
-      (%(M,N,f). Abs_hypreal(\<Union>X \<in> Rep_hypnat(M). \<Union>Y \<in> Rep_hypnat(N).  
-                             hyprel ``{%n::nat. setsum f {X n..<Y n}})) p"
+      (%(M,N,f). Abs_star(\<Union>X \<in> Rep_hypnat(M). \<Union>Y \<in> Rep_hypnat(N).  
+                             starrel ``{%n::nat. setsum f {X n..<Y n}})) p"
 
   NSsums  :: "[nat=>real,real] => bool"     (infixr "NSsums" 80)
    "f NSsums s  == (%n. setsum f {0..<n}) ----NS> s"
@@ -30,9 +30,9 @@
 lemma sumhr: 
      "sumhr(Abs_hypnat(hypnatrel``{%n. M n}),  
             Abs_hypnat(hypnatrel``{%n. N n}), f) =  
-      Abs_hypreal(hyprel `` {%n. setsum f {M n..<N n}})"
+      Abs_star(starrel `` {%n. setsum f {M n..<N n}})"
 apply (simp add: sumhr_def)
-apply (rule arg_cong [where f = Abs_hypreal])
+apply (rule arg_cong [where f = Abs_star])
 apply (auto, ultra)
 done
 
@@ -78,7 +78,7 @@
 
 lemma sumhr_mult: "hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)"
 apply (cases m, cases n)
-apply (simp add: sumhr hypreal_of_real_def hypreal_mult setsum_mult)
+apply (simp add: sumhr hypreal_of_real_def star_of_def star_n_def hypreal_mult setsum_mult)
 done
 
 lemma sumhr_split_add: "n < p ==> sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)"
@@ -107,6 +107,7 @@
      "sumhr(0, n, %i. r) = hypreal_of_hypnat n * hypreal_of_real r"
 apply (cases n)
 apply (simp add: sumhr hypnat_zero_def hypreal_of_real_def hypreal_of_hypnat 
+                 star_of_def star_n_def
                  hypreal_mult real_of_nat_def)
 done
 
@@ -139,7 +140,7 @@
 
 lemma sumhr_hypreal_omega_minus_one: "sumhr(0, whn, %i. 1) = omega - 1"
 by (simp add: hypnat_omega_def hypnat_zero_def omega_def hypreal_one_def
-              sumhr hypreal_diff real_of_nat_def)
+              sumhr hypreal_diff real_of_nat_def star_n_def)
 
 lemma sumhr_minus_one_realpow_zero [simp]: 
      "sumhr(0, whn + whn, %i. (-1) ^ (i+1)) = 0"
@@ -152,7 +153,7 @@
       ==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) =  
           (hypreal_of_nat (na - m) * hypreal_of_real r)"
 by(simp add: sumhr hypreal_of_nat_eq hypnat_of_nat_eq hypreal_of_real_def
-             real_of_nat_def hypreal_mult cong: setsum_ivl_cong)
+             real_of_nat_def star_of_def star_n_def hypreal_mult cong: setsum_ivl_cong)
 
 lemma starfunNat_sumr: "( *fNat* (%n. setsum f {0..<n})) N = sumhr(0,N,f)"
 apply (cases N)
diff -r 17256fe71aca -r ad73fb6144cf src/HOL/Hyperreal/HTranscendental.thy
--- a/src/HOL/Hyperreal/HTranscendental.thy	Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Hyperreal/HTranscendental.thy	Tue Sep 06 23:16:48 2005 +0200
@@ -54,13 +54,13 @@
 by (simp add: starfun hypreal_one_num)
 
 lemma hypreal_sqrt_pow2_iff: "(( *f* sqrt)(x) ^ 2 = x) = (0 \<le> x)"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
 apply (auto simp add: hypreal_le hypreal_zero_num starfun hrealpow 
             simp del: hpowr_Suc realpow_Suc)
 done
 
 lemma hypreal_sqrt_gt_zero_pow2: "0 < x ==> ( *f* sqrt) (x) ^ 2 = x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
 apply (auto intro: FreeUltrafilterNat_subset 
             simp add: hypreal_less starfun hrealpow hypreal_zero_num 
             simp del: hpowr_Suc realpow_Suc)
@@ -82,7 +82,7 @@
 
 lemma hypreal_sqrt_mult_distrib: 
     "[|0 < x; 0 <y |] ==> ( *f* sqrt)(x*y) =  ( *f* sqrt)(x) * ( *f* sqrt)(y)"
-apply (cases x, cases y)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
 apply (simp add: hypreal_zero_def starfun hypreal_mult hypreal_less hypreal_zero_num, ultra)
 apply (auto intro: real_sqrt_mult_distrib) 
 done
@@ -120,7 +120,7 @@
 done
 
 lemma hypreal_sqrt_gt_zero: "0 < x ==> 0 < ( *f* sqrt)(x)"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
 apply (auto simp add: starfun hypreal_zero_def hypreal_less hypreal_zero_num, ultra)
 apply (auto intro: real_sqrt_gt_zero)
 done
@@ -129,7 +129,7 @@
 by (auto intro: hypreal_sqrt_gt_zero simp add: order_le_less)
 
 lemma hypreal_sqrt_hrabs [simp]: "( *f* sqrt)(x ^ 2) = abs(x)"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
 apply (simp add: starfun hypreal_hrabs hypreal_mult numeral_2_eq_2)
 done
 
@@ -141,7 +141,7 @@
 
 lemma hypreal_sqrt_hyperpow_hrabs [simp]:
      "( *f* sqrt)(x pow (hypnat_of_nat 2)) = abs(x)"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
 apply (simp add: starfun hypreal_hrabs hypnat_of_nat_eq hyperpow)
 done
 
@@ -161,7 +161,7 @@
 done
 
 lemma hypreal_sqrt_sum_squares_ge1 [simp]: "x \<le> ( *f* sqrt)(x ^ 2 + y ^ 2)"
-apply (cases x, cases y)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
 apply (simp add: starfun hypreal_add hrealpow hypreal_le 
             del: hpowr_Suc realpow_Suc)
 done
@@ -292,7 +292,7 @@
 by (auto intro: STAR_exp_Infinitesimal)
 
 lemma STAR_exp_add: "( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y"
-apply (cases x, cases y)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
 apply (simp add: starfun hypreal_add hypreal_mult exp_add)
 done
 
@@ -301,7 +301,7 @@
 apply (rule st_hypreal_of_real [THEN subst])
 apply (rule approx_st_eq, auto)
 apply (rule approx_minus_iff [THEN iffD2])
-apply (auto simp add: mem_infmal_iff [symmetric] hypreal_of_real_def hypnat_zero_def hypnat_omega_def sumhr hypreal_minus hypreal_add)
+apply (auto simp add: mem_infmal_iff [symmetric] hypreal_of_real_def star_of_def star_n_def hypnat_zero_def hypnat_omega_def sumhr hypreal_minus hypreal_add)
 apply (rule NSLIMSEQ_zero_Infinitesimal_hypreal)
 apply (insert exp_converges [of x]) 
 apply (simp add: sums_def) 
@@ -310,7 +310,7 @@
 done
 
 lemma starfun_exp_ge_add_one_self [simp]: "0 \<le> x ==> (1 + x) \<le> ( *f* exp) x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
 apply (simp add: starfun hypreal_add hypreal_le hypreal_zero_num hypreal_one_num, ultra)
 apply (erule exp_ge_add_one_self_aux)
 done
@@ -324,7 +324,7 @@
 done
 
 lemma starfun_exp_minus: "( *f* exp) (-x) = inverse(( *f* exp) x)"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
 apply (simp add: starfun hypreal_inverse hypreal_minus exp_minus)
 done
 
@@ -338,7 +338,7 @@
 done
 
 lemma starfun_exp_gt_one [simp]: "0 < x ==> 1 < ( *f* exp) x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
 apply (simp add: starfun hypreal_one_num hypreal_zero_num hypreal_less, ultra)
 done
 
@@ -346,7 +346,7 @@
    TRY a NS one today!!!
 
 Goal "x @= 1 ==> ( *f* ln) x @= 1"
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","x")] eq_Abs_star 1);
 by (auto_tac (claset(),simpset() addsimps [hypreal_one_def]));
 
 
@@ -356,12 +356,12 @@
 
 
 lemma starfun_ln_exp [simp]: "( *f* ln) (( *f* exp) x) = x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
 apply (simp add: starfun)
 done
 
 lemma starfun_exp_ln_iff [simp]: "(( *f* exp)(( *f* ln) x) = x) = (0 < x)"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
 apply (simp add: starfun hypreal_zero_num hypreal_less)
 done
 
@@ -369,22 +369,22 @@
 by (auto simp add: starfun)
 
 lemma starfun_ln_less_self [simp]: "0 < x ==> ( *f* ln) x < x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
 apply (simp add: starfun hypreal_zero_num hypreal_less, ultra)
 done
 
 lemma starfun_ln_ge_zero [simp]: "1 \<le> x ==> 0 \<le> ( *f* ln) x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
 apply (simp add: starfun hypreal_zero_num hypreal_le hypreal_one_num, ultra)
 done
 
 lemma starfun_ln_gt_zero [simp]: "1 < x ==> 0 < ( *f* ln) x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
 apply (simp add: starfun hypreal_zero_num hypreal_less hypreal_one_num, ultra)
 done
 
 lemma starfun_ln_not_eq_zero [simp]: "[| 0 < x; x \<noteq> 1 |] ==> ( *f* ln) x \<noteq> 0"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
 apply (auto simp add: starfun hypreal_zero_num hypreal_less hypreal_one_num, ultra)
 done
 
@@ -395,15 +395,15 @@
 done
 
 lemma starfun_ln_inverse: "0 < x ==> ( *f* ln) (inverse x) = -( *f* ln) x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
 apply (simp add: starfun hypreal_zero_num hypreal_minus hypreal_inverse hypreal_less, ultra)
 apply (simp add: ln_inverse)
 done
 
 lemma starfun_exp_HFinite: "x \<in> HFinite ==> ( *f* exp) x \<in> HFinite"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
 apply (auto simp add: starfun HFinite_FreeUltrafilterNat_iff)
-apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
+apply (rule bexI, rule_tac [2] lemma_starrel_refl, auto)
 apply (rule_tac x = "exp u" in exI)
 apply (ultra, arith)
 done
@@ -449,7 +449,7 @@
 done
 
 lemma starfun_ln_less_zero: "[| 0 < x; x < 1 |] ==> ( *f* ln) x < 0"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
 apply (simp add: hypreal_zero_num hypreal_one_num hypreal_less starfun, ultra)
 done
 
diff -r 17256fe71aca -r ad73fb6144cf src/HOL/Hyperreal/HyperArith.thy
--- a/src/HOL/Hyperreal/HyperArith.thy	Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Hyperreal/HyperArith.thy	Tue Sep 06 23:16:48 2005 +0200
@@ -13,6 +13,7 @@
 
 subsection{*Numerals and Arithmetic*}
 
+(*
 instance hypreal :: number ..
 
 defs (overloaded)
@@ -21,11 +22,11 @@
 
 instance hypreal :: number_ring
 by (intro_classes, simp add: hypreal_number_of_def) 
-
+*)
 
 text{*Collapse applications of @{term hypreal_of_real} to @{term number_of}*}
 lemma hypreal_number_of [simp]: "hypreal_of_real (number_of w) = number_of w"
-by (simp add: hypreal_number_of_def real_number_of_def) 
+by (simp add: hypreal_of_real_def)
 
 
 
@@ -130,10 +131,11 @@
 done
 
 lemma hypreal_of_nat:
-     "hypreal_of_nat m = Abs_hypreal(hyprel``{%n. real m})"
-apply (induct m) 
-apply (simp_all add: hypreal_of_nat_def real_of_nat_def hypreal_zero_def 
-                     hypreal_one_def hypreal_add)
+     "hypreal_of_nat m = Abs_star(starrel``{%n. real m})"
+apply (fold star_n_def star_of_def)
+apply (induct m)
+apply (simp_all add: hypreal_of_nat_def real_of_nat_def
+                     hypreal_add)
 done
 
 lemma hypreal_of_nat_Suc:
diff -r 17256fe71aca -r ad73fb6144cf src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy	Tue Sep 06 23:16:48 2005 +0200
@@ -8,10 +8,13 @@
 header{*Construction of Hyperreals Using Ultrafilters*}
 
 theory HyperDef
-imports Filter "../Real/Real"
+(*imports Filter "../Real/Real"*)
+imports StarClasses "../Real/Real"
 uses ("fuf.ML")  (*Warning: file fuf.ML refers to the name Hyperdef!*)
 begin
 
+types hypreal = "real star"
+(*
 constdefs
 
   FreeUltrafilterNat   :: "nat set set"    ("\<U>")
@@ -46,17 +49,33 @@
 
   hypreal_divide_def:
   "P / Q::hypreal == P * inverse Q"
+*)
+
+lemma hypreal_zero_def: "0 == Abs_star(starrel``{%n. 0})"
+by (simp only: star_zero_def star_of_def star_n_def)
+
+lemma hypreal_one_def: "1 == Abs_star(starrel``{%n. 1})"
+by (simp only: star_one_def star_of_def star_n_def)
+
+lemma hypreal_diff_def: "x - y == x + -(y::hypreal)"
+by (rule diff_def)
+
+lemma hypreal_divide_def: "P / Q::hypreal == P * inverse Q"
+by (rule divide_inverse [THEN eq_reflection])
 
 constdefs
 
   hypreal_of_real  :: "real => hypreal"
-  "hypreal_of_real r         == Abs_hypreal(hyprel``{%n. r})"
+(*  "hypreal_of_real r         == Abs_hypreal(hyprel``{%n. r})" *)
+  "hypreal_of_real r == star_of r"
 
   omega   :: hypreal   -- {*an infinite number @{text "= [<1,2,3,...>]"} *}
-  "omega == Abs_hypreal(hyprel``{%n. real (Suc n)})"
+(*  "omega == Abs_hypreal(hyprel``{%n. real (Suc n)})" *)
+  "omega == star_n (%n. real (Suc n))"
 
   epsilon :: hypreal   -- {*an infinitesimal number @{text "= [<1,1/2,1/3,...>]"} *}
-  "epsilon == Abs_hypreal(hyprel``{%n. inverse (real (Suc n))})"
+(*  "epsilon == Abs_hypreal(hyprel``{%n. inverse (real (Suc n))})" *)
+  "epsilon == star_n (%n. inverse (real (Suc n)))"
 
 syntax (xsymbols)
   omega   :: hypreal   ("\<omega>")
@@ -66,7 +85,7 @@
   omega   :: hypreal   ("\<omega>")
   epsilon :: hypreal   ("\<epsilon>")
 
-
+(*
 defs (overloaded)
 
   hypreal_add_def:
@@ -85,7 +104,7 @@
   hypreal_less_def: "(x < (y::hypreal)) == (x \<le> y & x \<noteq> y)"
 
   hrabs_def:  "abs (r::hypreal) == (if 0 \<le> r then r else -r)"
-
+*)
 
 subsection{*The Set of Naturals is not Finite*}
 
@@ -116,7 +135,7 @@
 lemma FreeUltrafilterNat_Ex: "\<exists>U::nat set set. freeultrafilter U"
 by (rule not_finite_nat [THEN freeultrafilter_Ex])
 
-lemma FreeUltrafilterNat_mem [simp]: "freeultrafilter FreeUltrafilterNat"
+lemma FreeUltrafilterNat_mem: "freeultrafilter FreeUltrafilterNat"
 apply (unfold FreeUltrafilterNat_def)
 apply (rule someI_ex)
 apply (rule FreeUltrafilterNat_Ex)
@@ -210,53 +229,49 @@
 by (auto, ultra)
 
 
-subsection{*Properties of @{term hyprel}*}
+subsection{*Properties of @{term starrel}*}
 
-text{*Proving that @{term hyprel} is an equivalence relation*}
+text{*Proving that @{term starrel} is an equivalence relation*}
 
-lemma hyprel_iff: "((X,Y) \<in> hyprel) = ({n. X n = Y n} \<in> FreeUltrafilterNat)"
-by (simp add: hyprel_def)
+lemma starrel_iff: "((X,Y) \<in> starrel) = ({n. X n = Y n} \<in> FreeUltrafilterNat)"
+by (simp add: starrel_def)
 
-lemma hyprel_refl: "(x,x) \<in> hyprel"
-by (simp add: hyprel_def)
+lemma starrel_refl: "(x,x) \<in> starrel"
+by (simp add: starrel_def)
 
-lemma hyprel_sym [rule_format (no_asm)]: "(x,y) \<in> hyprel --> (y,x) \<in> hyprel"
-by (simp add: hyprel_def eq_commute)
+lemma starrel_sym [rule_format (no_asm)]: "(x,y) \<in> starrel --> (y,x) \<in> starrel"
+by (simp add: starrel_def eq_commute)
 
-lemma hyprel_trans: 
-      "[|(x,y) \<in> hyprel; (y,z) \<in> hyprel|] ==> (x,z) \<in> hyprel"
-by (simp add: hyprel_def, ultra)
+lemma starrel_trans: 
+      "[|(x,y) \<in> starrel; (y,z) \<in> starrel|] ==> (x,z) \<in> starrel"
+by (simp add: starrel_def, ultra)
 
-lemma equiv_hyprel: "equiv UNIV hyprel"
-apply (simp add: equiv_def refl_def sym_def trans_def hyprel_refl)
-apply (blast intro: hyprel_sym hyprel_trans) 
-done
+lemma equiv_starrel: "equiv UNIV starrel"
+by (rule StarType.equiv_starrel)
 
-(* (hyprel `` {x} = hyprel `` {y}) = ((x,y) \<in> hyprel) *)
-lemmas equiv_hyprel_iff =
-    eq_equiv_class_iff [OF equiv_hyprel UNIV_I UNIV_I, simp] 
+(* (starrel `` {x} = starrel `` {y}) = ((x,y) \<in> starrel) *)
+lemmas equiv_starrel_iff =
+    eq_equiv_class_iff [OF equiv_starrel UNIV_I UNIV_I, simp] 
 
-lemma hyprel_in_hypreal [simp]: "hyprel``{x}:hypreal"
-by (simp add: hypreal_def hyprel_def quotient_def, blast)
+lemma starrel_in_hypreal [simp]: "starrel``{x}:star"
+by (simp add: star_def starrel_def quotient_def, blast)
 
+declare Abs_star_inject [simp] Abs_star_inverse [simp]
+declare equiv_starrel [THEN eq_equiv_class_iff, simp]
+declare starrel_iff [iff]
 
-declare Abs_hypreal_inject [simp] Abs_hypreal_inverse [simp]
-declare equiv_hyprel [THEN eq_equiv_class_iff, simp]
-declare hyprel_iff [iff]
+lemmas eq_starrelD = eq_equiv_class [OF _ equiv_starrel]
 
-lemmas eq_hyprelD = eq_equiv_class [OF _ equiv_hyprel]
+lemma lemma_starrel_refl [simp]: "x \<in> starrel `` {x}"
+by (simp add: starrel_def)
 
-lemma lemma_hyprel_refl [simp]: "x \<in> hyprel `` {x}"
-by (simp add: hyprel_def)
-
-lemma hypreal_empty_not_mem [simp]: "{} \<notin> hypreal"
-apply (simp add: hypreal_def)
+lemma hypreal_empty_not_mem [simp]: "{} \<notin> star"
+apply (simp add: star_def)
 apply (auto elim!: quotientE equalityCE)
 done
 
-lemma Rep_hypreal_nonempty [simp]: "Rep_hypreal x \<noteq> {}"
-by (insert Rep_hypreal [of x], auto)
-
+lemma Rep_hypreal_nonempty [simp]: "Rep_star x \<noteq> {}"
+by (insert Rep_star [of x], auto)
 
 subsection{*@{term hypreal_of_real}: 
             the Injection from @{typ real} to @{typ hypreal}*}
@@ -266,128 +281,116 @@
 apply (simp add: hypreal_of_real_def split: split_if_asm)
 done
 
-lemma eq_Abs_hypreal:
-    "(!!x. z = Abs_hypreal(hyprel``{x}) ==> P) ==> P"
-apply (rule_tac x1=z in Rep_hypreal [unfolded hypreal_def, THEN quotientE])
-apply (drule_tac f = Abs_hypreal in arg_cong)
-apply (force simp add: Rep_hypreal_inverse)
-done
+lemma eq_Abs_star:
+    "(!!x. z = Abs_star(starrel``{x}) ==> P) ==> P"
+by (fold star_n_def, auto intro: star_cases)
 
+(*
 theorem hypreal_cases [case_names Abs_hypreal, cases type: hypreal]:
-    "(!!x. z = Abs_hypreal(hyprel``{x}) ==> P) ==> P"
+    "(!!x. z = star_n x ==> P) ==> P"
 by (rule eq_Abs_hypreal [of z], blast)
-
+*)
 
 subsection{*Hyperreal Addition*}
-
+(*
 lemma hypreal_add_congruent2: 
-    "congruent2 hyprel hyprel (%X Y. hyprel``{%n. X n + Y n})"
+    "congruent2 starrel starrel (%X Y. starrel``{%n. X n + Y n})"
 by (simp add: congruent2_def, auto, ultra)
-
-lemma hypreal_add: 
-  "Abs_hypreal(hyprel``{%n. X n}) + Abs_hypreal(hyprel``{%n. Y n}) =  
-   Abs_hypreal(hyprel``{%n. X n + Y n})"
-by (simp add: hypreal_add_def 
-         UN_equiv_class2 [OF equiv_hyprel equiv_hyprel hypreal_add_congruent2])
+*)
+lemma hypreal_add [unfolded star_n_def]: 
+  "star_n X + star_n Y = star_n (%n. X n + Y n)"
+by (simp add: star_add_def Ifun2_of_def star_of_def Ifun_star_n)
 
 lemma hypreal_add_commute: "(z::hypreal) + w = w + z"
-apply (cases z, cases w)
-apply (simp add: add_ac hypreal_add)
-done
+by (rule add_commute)
 
 lemma hypreal_add_assoc: "((z1::hypreal) + z2) + z3 = z1 + (z2 + z3)"
-apply (cases z1, cases z2, cases z3)
-apply (simp add: hypreal_add real_add_assoc)
-done
+by (rule add_assoc)
 
 lemma hypreal_add_zero_left: "(0::hypreal) + z = z"
-by (cases z, simp add: hypreal_zero_def hypreal_add)
+by (rule comm_monoid_add_class.add_0)
 
-instance hypreal :: comm_monoid_add
+(*instance hypreal :: comm_monoid_add
   by intro_classes
     (assumption | 
-      rule hypreal_add_commute hypreal_add_assoc hypreal_add_zero_left)+
+      rule hypreal_add_commute hypreal_add_assoc hypreal_add_zero_left)+*)
 
 lemma hypreal_add_zero_right [simp]: "z + (0::hypreal) = z"
-by (simp add: hypreal_add_zero_left hypreal_add_commute)
+by (rule OrderedGroup.add_0_right)
 
 
 subsection{*Additive inverse on @{typ hypreal}*}
-
-lemma hypreal_minus_congruent: "(%X. hyprel``{%n. - (X n)}) respects hyprel"
+(*
+lemma hypreal_minus_congruent: "(%X. starrel``{%n. - (X n)}) respects starrel"
 by (force simp add: congruent_def)
+*)
+lemma hypreal_minus [unfolded star_n_def]: 
+   "- star_n X = star_n (%n. -(X n))"
+by (simp add: star_minus_def Ifun_of_def star_of_def Ifun_star_n)
 
-lemma hypreal_minus: 
-   "- (Abs_hypreal(hyprel``{%n. X n})) = Abs_hypreal(hyprel `` {%n. -(X n)})"
-by (simp add: hypreal_minus_def hyprel_in_hypreal [THEN Abs_hypreal_inverse] 
-              UN_equiv_class [OF equiv_hyprel hypreal_minus_congruent])
-
-lemma hypreal_diff:
-     "Abs_hypreal(hyprel``{%n. X n}) - Abs_hypreal(hyprel``{%n. Y n}) =  
-      Abs_hypreal(hyprel``{%n. X n - Y n})"
-by (simp add: hypreal_diff_def hypreal_minus hypreal_add)
+lemma hypreal_diff [unfolded star_n_def]:
+     "star_n X - star_n Y = star_n (%n. X n - Y n)"
+by (simp add: star_diff_def Ifun2_of_def star_of_def Ifun_star_n)
 
 lemma hypreal_add_minus [simp]: "z + -z = (0::hypreal)"
-by (cases z, simp add: hypreal_zero_def hypreal_minus hypreal_add)
+by (rule right_minus)
 
 lemma hypreal_add_minus_left: "-z + z = (0::hypreal)"
-by (simp add: hypreal_add_commute)
+by (rule left_minus)
 
 
 subsection{*Hyperreal Multiplication*}
-
+(*
 lemma hypreal_mult_congruent2: 
-    "congruent2 hyprel hyprel (%X Y. hyprel``{%n. X n * Y n})"
+    "congruent2 starrel starrel (%X Y. starrel``{%n. X n * Y n})"
 by (simp add: congruent2_def, auto, ultra)
+*)
 
-lemma hypreal_mult: 
-  "Abs_hypreal(hyprel``{%n. X n}) * Abs_hypreal(hyprel``{%n. Y n}) =  
-   Abs_hypreal(hyprel``{%n. X n * Y n})"
-by (simp add: hypreal_mult_def
-        UN_equiv_class2 [OF equiv_hyprel equiv_hyprel hypreal_mult_congruent2])
+lemma hypreal_mult [unfolded star_n_def]: 
+  "star_n X * star_n Y = star_n (%n. X n * Y n)"
+by (simp add: star_mult_def Ifun2_of_def star_of_def Ifun_star_n)
 
 lemma hypreal_mult_commute: "(z::hypreal) * w = w * z"
-by (cases z, cases w, simp add: hypreal_mult mult_ac)
+by (rule mult_commute)
 
 lemma hypreal_mult_assoc: "((z1::hypreal) * z2) * z3 = z1 * (z2 * z3)"
-by (cases z1, cases z2, cases z3, simp add: hypreal_mult mult_assoc)
+by (rule mult_assoc)
 
 lemma hypreal_mult_1: "(1::hypreal) * z = z"
-by (cases z, simp add: hypreal_one_def hypreal_mult)
+by (rule mult_1_left)
 
 lemma hypreal_add_mult_distrib:
      "((z1::hypreal) + z2) * w = (z1 * w) + (z2 * w)"
-by (cases z1, cases z2, cases w, simp add: hypreal_mult hypreal_add left_distrib)
+by (rule left_distrib)
 
 text{*one and zero are distinct*}
 lemma hypreal_zero_not_eq_one: "0 \<noteq> (1::hypreal)"
-by (simp add: hypreal_zero_def hypreal_one_def)
+by (rule zero_neq_one)
 
 
 subsection{*Multiplicative Inverse on @{typ hypreal} *}
-
+(*
 lemma hypreal_inverse_congruent: 
-  "(%X. hyprel``{%n. if X n = 0 then 0 else inverse(X n)}) respects hyprel"
+  "(%X. starrel``{%n. if X n = 0 then 0 else inverse(X n)}) respects starrel"
 by (auto simp add: congruent_def, ultra)
-
-lemma hypreal_inverse: 
-      "inverse (Abs_hypreal(hyprel``{%n. X n})) =  
-       Abs_hypreal(hyprel `` {%n. if X n = 0 then 0 else inverse(X n)})"
-by (simp add: hypreal_inverse_def hyprel_in_hypreal [THEN Abs_hypreal_inverse] 
-              UN_equiv_class [OF equiv_hyprel hypreal_inverse_congruent])
+*)
+lemma hypreal_inverse [unfolded star_n_def]: 
+      "inverse (star_n X) = star_n (%n. if X n = (0::real) then 0 else inverse(X n))"
+apply (simp add: star_inverse_def Ifun_of_def star_of_def Ifun_star_n)
+apply (rule_tac f=star_n in arg_cong)
+apply (rule ext)
+apply simp
+done
 
 lemma hypreal_mult_inverse: 
      "x \<noteq> 0 ==> x*inverse(x) = (1::hypreal)"
-apply (cases x)
-apply (simp add: hypreal_one_def hypreal_zero_def hypreal_inverse hypreal_mult)
-apply (drule FreeUltrafilterNat_Compl_mem)
-apply (blast intro!: right_inverse FreeUltrafilterNat_subset)
-done
+by (rule right_inverse)
 
 lemma hypreal_mult_inverse_left:
      "x \<noteq> 0 ==> inverse(x)*x = (1::hypreal)"
-by (simp add: hypreal_mult_inverse hypreal_mult_commute)
+by (rule left_inverse)
 
+(*
 instance hypreal :: field
 proof
   fix x y z :: hypreal
@@ -408,62 +411,57 @@
   show "inverse 0 = (0::hypreal)" 
     by (simp add: hypreal_inverse hypreal_zero_def)
 qed
-
+*)
 
 subsection{*Properties of The @{text "\<le>"} Relation*}
 
-lemma hypreal_le: 
-      "(Abs_hypreal(hyprel``{%n. X n}) \<le> Abs_hypreal(hyprel``{%n. Y n})) =  
+lemma hypreal_le [unfolded star_n_def]: 
+      "star_n X \<le> star_n Y =  
        ({n. X n \<le> Y n} \<in> FreeUltrafilterNat)"
-apply (simp add: hypreal_le_def)
-apply (auto intro!: lemma_hyprel_refl, ultra)
-done
+by (simp add: star_le_def Ipred2_of_def star_of_def Ifun_star_n unstar_star_n)
 
 lemma hypreal_le_refl: "w \<le> (w::hypreal)"
-by (cases w, simp add: hypreal_le)
+by (rule order_refl)
 
 lemma hypreal_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::hypreal)"
-by (cases i, cases j, cases k, simp add: hypreal_le, ultra)
+by (rule order_trans)
 
 lemma hypreal_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::hypreal)"
-by (cases z, cases w, simp add: hypreal_le, ultra)
+by (rule order_antisym)
 
 (* Axiom 'order_less_le' of class 'order': *)
 lemma hypreal_less_le: "((w::hypreal) < z) = (w \<le> z & w \<noteq> z)"
-by (simp add: hypreal_less_def)
+by (rule order_less_le)
 
+(*
 instance hypreal :: order
   by intro_classes
     (assumption |
       rule hypreal_le_refl hypreal_le_trans hypreal_le_anti_sym hypreal_less_le)+
-
+*)
 
 (* Axiom 'linorder_linear' of class 'linorder': *)
 lemma hypreal_le_linear: "(z::hypreal) \<le> w | w \<le> z"
-apply (cases z, cases w)
-apply (auto simp add: hypreal_le, ultra)
-done
+by (rule linorder_linear)
 
+(*
 instance hypreal :: linorder 
   by intro_classes (rule hypreal_le_linear)
+*)
 
 lemma hypreal_not_refl2: "!!(x::hypreal). x < y ==> x \<noteq> y"
 by (auto)
 
 lemma hypreal_add_left_mono: "x \<le> y ==> z + x \<le> z + (y::hypreal)"
-apply (cases x, cases y, cases z)
-apply (auto simp add: hypreal_le hypreal_add) 
-done
+by (rule add_left_mono)
 
 lemma hypreal_mult_less_mono2: "[| (0::hypreal)<z; x<y |] ==> z*x<z*y"
-apply (cases x, cases y, cases z)
-apply (auto simp add: hypreal_zero_def hypreal_le hypreal_mult 
-                      linorder_not_le [symmetric], ultra) 
-done
+by (rule mult_strict_left_mono)
 
 
 subsection{*The Hyperreals Form an Ordered Field*}
 
+(*
 instance hypreal :: ordered_field
 proof
   fix x y z :: hypreal
@@ -474,6 +472,7 @@
   show "\<bar>x\<bar> = (if x < 0 then -x else x)"
     by (auto dest: order_le_less_trans simp add: hrabs_def linorder_not_le)
 qed
+*)
 
 lemma hypreal_eq_minus_iff: "((x::hypreal) = y) = (x + - y = 0)"
 by auto
@@ -490,41 +489,37 @@
 
 lemma hypreal_of_real_add [simp]: 
      "hypreal_of_real (w + z) = hypreal_of_real w + hypreal_of_real z"
-by (simp add: hypreal_of_real_def, simp add: hypreal_add left_distrib)
+by (simp add: hypreal_of_real_def)
 
 lemma hypreal_of_real_minus [simp]:
      "hypreal_of_real (-r) = - hypreal_of_real  r"
-by (auto simp add: hypreal_of_real_def hypreal_minus)
+by (simp add: hypreal_of_real_def)
 
 lemma hypreal_of_real_diff [simp]: 
      "hypreal_of_real (w - z) = hypreal_of_real w - hypreal_of_real z"
-by (simp add: diff_minus) 
+by (simp add: hypreal_of_real_def)
 
 lemma hypreal_of_real_mult [simp]: 
      "hypreal_of_real (w * z) = hypreal_of_real w * hypreal_of_real z"
-by (simp add: hypreal_of_real_def, simp add: hypreal_mult right_distrib)
+by (simp add: hypreal_of_real_def)
 
 lemma hypreal_of_real_one [simp]: "hypreal_of_real 1 = (1::hypreal)"
-by (simp add: hypreal_of_real_def hypreal_one_def)
+by (simp add: hypreal_of_real_def)
 
 lemma hypreal_of_real_zero [simp]: "hypreal_of_real 0 = 0"
-by (simp add: hypreal_of_real_def hypreal_zero_def)
+by (simp add: hypreal_of_real_def)
 
 lemma hypreal_of_real_le_iff [simp]: 
      "(hypreal_of_real w \<le> hypreal_of_real z) = (w \<le> z)"
-apply (simp add: hypreal_le_def hypreal_of_real_def, auto)
-apply (rule_tac [2] x = "%n. w" in exI, safe)
-apply (rule_tac [3] x = "%n. z" in exI, auto)
-apply (rule FreeUltrafilterNat_P, ultra)
-done
+by (simp add: hypreal_of_real_def)
 
 lemma hypreal_of_real_less_iff [simp]: 
      "(hypreal_of_real w < hypreal_of_real z) = (w < z)"
-by (simp add: linorder_not_le [symmetric]) 
+by (simp add: hypreal_of_real_def)
 
 lemma hypreal_of_real_eq_iff [simp]:
      "(hypreal_of_real w = hypreal_of_real z) = (w = z)"
-by (force intro: order_antisym hypreal_of_real_le_iff [THEN iffD1])
+by (simp add: hypreal_of_real_def)
 
 text{*As above, for 0*}
 
@@ -548,60 +543,45 @@
 
 lemma hypreal_of_real_inverse [simp]:
      "hypreal_of_real (inverse r) = inverse (hypreal_of_real r)"
-apply (case_tac "r=0", simp)
-apply (rule_tac c1 = "hypreal_of_real r" in hypreal_mult_left_cancel [THEN iffD1])
-apply (auto simp add: hypreal_of_real_mult [symmetric])
-done
+by (simp add: hypreal_of_real_def)
 
 lemma hypreal_of_real_divide [simp]:
      "hypreal_of_real (w / z) = hypreal_of_real w / hypreal_of_real z"
-by (simp add: hypreal_divide_def real_divide_def)
+by (simp add: hypreal_of_real_def)
 
 lemma hypreal_of_real_of_nat [simp]: "hypreal_of_real (of_nat n) = of_nat n"
-by (induct n, simp_all) 
+by (simp add: hypreal_of_real_def)
 
 lemma hypreal_of_real_of_int [simp]:  "hypreal_of_real (of_int z) = of_int z"
-proof (cases z)
-  case (1 n)
-    thus ?thesis  by simp
-next
-  case (2 n)
-    thus ?thesis
-      by (simp only: of_int_minus hypreal_of_real_minus, simp)
-qed
+by (simp add: hypreal_of_real_def)
 
 
 subsection{*Misc Others*}
 
-lemma hypreal_less: 
-      "(Abs_hypreal(hyprel``{%n. X n}) < Abs_hypreal(hyprel``{%n. Y n})) =  
-       ({n. X n < Y n} \<in> FreeUltrafilterNat)"
-by (auto simp add: hypreal_le linorder_not_le [symmetric], ultra+)
+lemma hypreal_less [unfolded star_n_def]: 
+      "star_n X < star_n Y = ({n. X n < Y n} \<in> FreeUltrafilterNat)"
+by (simp add: star_less_def Ipred2_of_def star_of_def Ifun_star_n unstar_star_n)
 
-lemma hypreal_zero_num: "0 = Abs_hypreal (hyprel `` {%n. 0})"
-by (simp add: hypreal_zero_def [THEN meta_eq_to_obj_eq, symmetric])
+lemma hypreal_zero_num [unfolded star_n_def]: "0 = star_n (%n. 0)"
+by (simp add: star_zero_def star_of_def)
 
-lemma hypreal_one_num: "1 = Abs_hypreal (hyprel `` {%n. 1})"
-by (simp add: hypreal_one_def [THEN meta_eq_to_obj_eq, symmetric])
+lemma hypreal_one_num [unfolded star_n_def]: "1 = star_n (%n. 1)"
+by (simp add: star_one_def star_of_def)
 
 lemma hypreal_omega_gt_zero [simp]: "0 < omega"
-by (auto simp add: omega_def hypreal_less hypreal_zero_num)
-
-lemma hypreal_hrabs:
-     "abs (Abs_hypreal (hyprel `` {X})) = 
-      Abs_hypreal(hyprel `` {%n. abs (X n)})"
-apply (auto simp add: hrabs_def hypreal_zero_def hypreal_le hypreal_minus)
-apply ultra
-apply ultra
-apply arith
+apply (simp only: omega_def star_zero_def star_less_def star_of_def)
+apply (simp add: Ipred2_of_def star_of_def Ifun_star_n unstar_star_n)
 done
 
+lemma hypreal_hrabs [unfolded star_n_def]:
+     "abs (star_n X) = star_n (%n. abs (X n))"
+by (simp add: star_abs_def Ifun_of_def star_of_def Ifun_star_n)
 
 subsection{*Existence of Infinite Hyperreal Number*}
-
+(*
 lemma Rep_hypreal_omega: "Rep_hypreal(omega) \<in> hypreal"
 by (simp add: omega_def)
-
+*)
 text{*Existence of infinite number not corresponding to any real number.
 Use assumption that member @{term FreeUltrafilterNat} is not finite.*}
 
@@ -618,6 +598,7 @@
 lemma not_ex_hypreal_of_real_eq_omega: 
       "~ (\<exists>x. hypreal_of_real x = omega)"
 apply (simp add: omega_def hypreal_of_real_def)
+apply (simp add: star_of_def star_n_eq_iff)
 apply (auto simp add: real_of_nat_Suc diff_eq_eq [symmetric] 
             lemma_finite_omega_set [THEN FreeUltrafilterNat_finite])
 done
@@ -638,36 +619,40 @@
 
 lemma not_ex_hypreal_of_real_eq_epsilon: "~ (\<exists>x. hypreal_of_real x = epsilon)"
 by (auto simp add: epsilon_def hypreal_of_real_def 
+                   star_of_def star_n_eq_iff
                    lemma_finite_epsilon_set [THEN FreeUltrafilterNat_finite])
 
 lemma hypreal_of_real_not_eq_epsilon: "hypreal_of_real x \<noteq> epsilon"
 by (insert not_ex_hypreal_of_real_eq_epsilon, auto)
 
 lemma hypreal_epsilon_not_zero: "epsilon \<noteq> 0"
-by (simp add: epsilon_def hypreal_zero_def)
+by (simp add: epsilon_def star_zero_def star_of_def star_n_eq_iff
+         del: star_of_zero)
 
 lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)"
-by (simp add: hypreal_inverse omega_def epsilon_def)
+apply (simp add: epsilon_def omega_def star_inverse_def)
+apply (simp add: Ifun_of_def star_of_def Ifun_star_n)
+done
 
 
 ML
 {*
-val hrabs_def = thm "hrabs_def";
-val hypreal_hrabs = thm "hypreal_hrabs";
+(* val hrabs_def = thm "hrabs_def"; *)
+(* val hypreal_hrabs = thm "hypreal_hrabs"; *)
 
 val hypreal_zero_def = thm "hypreal_zero_def";
-val hypreal_one_def = thm "hypreal_one_def";
-val hypreal_minus_def = thm "hypreal_minus_def";
-val hypreal_diff_def = thm "hypreal_diff_def";
-val hypreal_inverse_def = thm "hypreal_inverse_def";
-val hypreal_divide_def = thm "hypreal_divide_def";
+(* val hypreal_one_def = thm "hypreal_one_def"; *)
+(* val hypreal_minus_def = thm "hypreal_minus_def"; *)
+(* val hypreal_diff_def = thm "hypreal_diff_def"; *)
+(* val hypreal_inverse_def = thm "hypreal_inverse_def"; *)
+(* val hypreal_divide_def = thm "hypreal_divide_def"; *)
 val hypreal_of_real_def = thm "hypreal_of_real_def";
 val omega_def = thm "omega_def";
 val epsilon_def = thm "epsilon_def";
-val hypreal_add_def = thm "hypreal_add_def";
-val hypreal_mult_def = thm "hypreal_mult_def";
-val hypreal_less_def = thm "hypreal_less_def";
-val hypreal_le_def = thm "hypreal_le_def";
+(* val hypreal_add_def = thm "hypreal_add_def"; *)
+(* val hypreal_mult_def = thm "hypreal_mult_def"; *)
+(* val hypreal_less_def = thm "hypreal_less_def"; *)
+(* val hypreal_le_def = thm "hypreal_le_def"; *)
 
 val finite_exhausts = thm "finite_exhausts";
 val finite_not_covers = thm "finite_not_covers";
@@ -689,15 +674,15 @@
 val FreeUltrafilterNat_Ex_P = thm "FreeUltrafilterNat_Ex_P";
 val FreeUltrafilterNat_all = thm "FreeUltrafilterNat_all";
 val FreeUltrafilterNat_Un = thm "FreeUltrafilterNat_Un";
-val hyprel_iff = thm "hyprel_iff";
-val hyprel_in_hypreal = thm "hyprel_in_hypreal";
-val Abs_hypreal_inverse = thm "Abs_hypreal_inverse";
-val lemma_hyprel_refl = thm "lemma_hyprel_refl";
+val starrel_iff = thm "starrel_iff";
+val starrel_in_hypreal = thm "starrel_in_hypreal";
+val Abs_star_inverse = thm "Abs_star_inverse";
+val lemma_starrel_refl = thm "lemma_starrel_refl";
 val hypreal_empty_not_mem = thm "hypreal_empty_not_mem";
 val Rep_hypreal_nonempty = thm "Rep_hypreal_nonempty";
 val inj_hypreal_of_real = thm "inj_hypreal_of_real";
-val eq_Abs_hypreal = thm "eq_Abs_hypreal";
-val hypreal_minus_congruent = thm "hypreal_minus_congruent";
+val eq_Abs_star = thm "eq_Abs_star";
+(* val hypreal_minus_congruent = thm "hypreal_minus_congruent"; *)
 val hypreal_minus = thm "hypreal_minus";
 val hypreal_add = thm "hypreal_add";
 val hypreal_diff = thm "hypreal_diff";
@@ -712,7 +697,7 @@
 val hypreal_mult_assoc = thm "hypreal_mult_assoc";
 val hypreal_mult_1 = thm "hypreal_mult_1";
 val hypreal_zero_not_eq_one = thm "hypreal_zero_not_eq_one";
-val hypreal_inverse_congruent = thm "hypreal_inverse_congruent";
+(* val hypreal_inverse_congruent = thm "hypreal_inverse_congruent"; *)
 val hypreal_inverse = thm "hypreal_inverse";
 val hypreal_mult_inverse = thm "hypreal_mult_inverse";
 val hypreal_mult_inverse_left = thm "hypreal_mult_inverse_left";
@@ -741,7 +726,7 @@
 val hypreal_one_num = thm "hypreal_one_num";
 val hypreal_omega_gt_zero = thm "hypreal_omega_gt_zero";
 
-val Rep_hypreal_omega = thm"Rep_hypreal_omega";
+(* val Rep_hypreal_omega = thm"Rep_hypreal_omega"; *)
 val lemma_omega_empty_singleton_disj = thm"lemma_omega_empty_singleton_disj";
 val lemma_finite_omega_set = thm"lemma_finite_omega_set";
 val not_ex_hypreal_of_real_eq_omega = thm"not_ex_hypreal_of_real_eq_omega";
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
 
diff -r 17256fe71aca -r ad73fb6144cf src/HOL/Hyperreal/HyperPow.thy
--- a/src/HOL/Hyperreal/HyperPow.thy	Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Hyperreal/HyperPow.thy	Tue Sep 06 23:16:48 2005 +0200
@@ -10,14 +10,14 @@
 imports HyperArith HyperNat
 begin
 
-instance hypreal :: power ..
+(* instance hypreal :: power .. *)
 
 consts hpowr :: "[hypreal,nat] => hypreal"  
+(*
 primrec
    hpowr_0:   "r ^ 0       = (1::hypreal)"
    hpowr_Suc: "r ^ (Suc n) = (r::hypreal) * (r ^ n)"
 
-
 instance hypreal :: recpower
 proof
   fix z :: hypreal
@@ -25,7 +25,13 @@
   show "z^0 = 1" by simp
   show "z^(Suc n) = z * (z^n)" by simp
 qed
+*)
 
+lemma hpowr_0 [simp]:   "r ^ 0       = (1::hypreal)"
+by (rule power_0)
+
+lemma hpowr_Suc [simp]: "r ^ (Suc n) = (r::hypreal) * (r ^ n)"
+by (rule power_Suc)
 
 consts
   "pow"  :: "[hypreal,hypnat] => hypreal"     (infixr 80)
@@ -35,8 +41,8 @@
   (* hypernatural powers of hyperreals *)
   hyperpow_def:
   "(R::hypreal) pow (N::hypnat) ==
-      Abs_hypreal(\<Union>X \<in> Rep_hypreal(R). \<Union>Y \<in> Rep_hypnat(N).
-                        hyprel``{%n::nat. (X n) ^ (Y n)})"
+      Abs_star(\<Union>X \<in> Rep_star(R). \<Union>Y \<in> Rep_hypnat(N).
+                        starrel``{%n::nat. (X n) ^ (Y n)})"
 
 lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r"
 by simp
@@ -84,9 +90,9 @@
 done
 
 lemma hrealpow:
-    "Abs_hypreal(hyprel``{%n. X n}) ^ m = Abs_hypreal(hyprel``{%n. (X n) ^ m})"
+    "Abs_star(starrel``{%n. X n}) ^ m = Abs_star(starrel``{%n. (X n::real) ^ m})"
 apply (induct_tac "m")
-apply (auto simp add: hypreal_one_def hypreal_mult)
+apply (auto simp add: hypreal_one_def hypreal_mult power_0)
 done
 
 lemma hrealpow_sum_square_expand:
@@ -115,16 +121,16 @@
 
 subsection{*Powers with Hypernatural Exponents*}
 
-lemma hyperpow_congruent: "(%X Y. hyprel``{%n. (X n ^ Y n)}) respects hyprel"
+lemma hyperpow_congruent: "(%X Y. starrel``{%n. (X n ^ Y n)}) respects starrel"
 by (auto simp add: congruent_def intro!: ext, fuf+)
 
 lemma hyperpow:
-  "Abs_hypreal(hyprel``{%n. X n}) pow Abs_hypnat(hypnatrel``{%n. Y n}) =
-   Abs_hypreal(hyprel``{%n. X n ^ Y n})"
+  "Abs_star(starrel``{%n. X n}) pow Abs_hypnat(hypnatrel``{%n. Y n}) =
+   Abs_star(starrel``{%n. X n ^ Y n})"
 apply (unfold hyperpow_def)
-apply (rule_tac f = Abs_hypreal in arg_cong)
-apply (auto intro!: lemma_hyprel_refl bexI 
-           simp add: hyprel_in_hypreal [THEN Abs_hypreal_inverse] equiv_hyprel 
+apply (rule_tac f = Abs_star in arg_cong)
+apply (auto intro!: lemma_starrel_refl bexI 
+           simp add: starrel_in_hypreal [THEN Abs_star_inverse] equiv_starrel 
                      hyperpow_congruent, fuf)
 done
 
@@ -138,54 +144,54 @@
 
 lemma hyperpow_not_zero [rule_format (no_asm)]:
      "r \<noteq> (0::hypreal) --> r pow n \<noteq> 0"
-apply (simp (no_asm) add: hypreal_zero_def, cases n, cases r)
+apply (simp (no_asm) add: hypreal_zero_def, cases n, rule_tac z=r in eq_Abs_star)
 apply (auto simp add: hyperpow)
 apply (drule FreeUltrafilterNat_Compl_mem, ultra)
 done
 
 lemma hyperpow_inverse:
      "r \<noteq> (0::hypreal) --> inverse(r pow n) = (inverse r) pow n"
-apply (simp (no_asm) add: hypreal_zero_def, cases n, cases r)
+apply (simp (no_asm) add: hypreal_zero_def, cases n, rule_tac z=r in eq_Abs_star)
 apply (auto dest!: FreeUltrafilterNat_Compl_mem simp add: hypreal_inverse hyperpow)
 apply (rule FreeUltrafilterNat_subset)
 apply (auto dest: realpow_not_zero intro: power_inverse)
 done
 
 lemma hyperpow_hrabs: "abs r pow n = abs (r pow n)"
-apply (cases n, cases r)
+apply (cases n, rule_tac z=r in eq_Abs_star)
 apply (auto simp add: hypreal_hrabs hyperpow power_abs [symmetric])
 done
 
 lemma hyperpow_add: "r pow (n + m) = (r pow n) * (r pow m)"
-apply (cases n, cases m, cases r)
+apply (cases n, cases m, rule_tac z=r in eq_Abs_star)
 apply (auto simp add: hyperpow hypnat_add hypreal_mult power_add)
 done
 
 lemma hyperpow_one [simp]: "r pow (1::hypnat) = r"
-apply (unfold hypnat_one_def, cases r)
+apply (unfold hypnat_one_def, rule_tac z=r in eq_Abs_star)
 apply (auto simp add: hyperpow)
 done
 
 lemma hyperpow_two:
      "r pow ((1::hypnat) + (1::hypnat)) = r * r"
-apply (unfold hypnat_one_def, cases r)
+apply (unfold hypnat_one_def, rule_tac z=r in eq_Abs_star)
 apply (auto simp add: hyperpow hypnat_add hypreal_mult)
 done
 
 lemma hyperpow_gt_zero: "(0::hypreal) < r ==> 0 < r pow n"
-apply (simp add: hypreal_zero_def, cases n, cases r)
+apply (simp add: hypreal_zero_def, cases n, rule_tac z=r in eq_Abs_star)
 apply (auto elim!: FreeUltrafilterNat_subset zero_less_power
                    simp add: hyperpow hypreal_less hypreal_le)
 done
 
 lemma hyperpow_ge_zero: "(0::hypreal) \<le> r ==> 0 \<le> r pow n"
-apply (simp add: hypreal_zero_def, cases n, cases r)
+apply (simp add: hypreal_zero_def, cases n, rule_tac z=r in eq_Abs_star)
 apply (auto elim!: FreeUltrafilterNat_subset zero_le_power 
             simp add: hyperpow hypreal_le)
 done
 
 lemma hyperpow_le: "[|(0::hypreal) < x; x \<le> y|] ==> x pow n \<le> y pow n"
-apply (simp add: hypreal_zero_def, cases n, cases x, cases y)
+apply (simp add: hypreal_zero_def, cases n, rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
 apply (auto simp add: hyperpow hypreal_le hypreal_less)
 apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset], assumption)
 apply (auto intro: power_mono)
@@ -204,7 +210,7 @@
 done
 
 lemma hyperpow_mult: "(r * s) pow n = (r pow n) * (s pow n)"
-apply (cases n, cases r, cases s)
+apply (cases n, rule_tac z=r in eq_Abs_star, rule_tac z=s in eq_Abs_star)
 apply (auto simp add: hyperpow hypreal_mult power_mult_distrib)
 done
 
@@ -248,7 +254,7 @@
 
 lemma hyperpow_less_le:
      "[|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n"
-apply (cases n, cases N, cases r)
+apply (cases n, cases N, rule_tac z=r in eq_Abs_star)
 apply (auto simp add: hyperpow hypreal_le hypreal_less hypnat_less 
             hypreal_zero_def hypreal_one_def)
 apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset])
@@ -263,7 +269,7 @@
 
 lemma hyperpow_realpow:
       "(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)"
-by (simp add: hypreal_of_real_def hypnat_of_nat_eq hyperpow)
+by (simp add: hypreal_of_real_def star_of_def star_n_def hypnat_of_nat_eq hyperpow)
 
 lemma hyperpow_SReal [simp]:
      "(hypreal_of_real r) pow (hypnat_of_nat n) \<in> Reals"
@@ -301,7 +307,7 @@
 
 lemma hrealpow_hyperpow_Infinitesimal_iff:
      "(x ^ n \<in> Infinitesimal) = (x pow (hypnat_of_nat n) \<in> Infinitesimal)"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
 apply (simp add: hrealpow hyperpow hypnat_of_nat_eq)
 done
 
diff -r 17256fe71aca -r ad73fb6144cf src/HOL/Hyperreal/Lim.thy
--- a/src/HOL/Hyperreal/Lim.thy	Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Hyperreal/Lim.thy	Tue Sep 06 23:16:48 2005 +0200
@@ -226,9 +226,9 @@
       "f -- x --> L ==> f -- x --NS> L"
 apply (simp add: LIM_def NSLIM_def approx_def)
 apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, safe)
-apply (rule_tac z = xa in eq_Abs_hypreal)
-apply (auto simp add: real_add_minus_iff starfun hypreal_minus hypreal_of_real_def hypreal_add)
-apply (rule bexI, rule_tac [2] lemma_hyprel_refl, clarify) 
+apply (rule_tac z = xa in eq_Abs_star)
+apply (auto simp add: real_add_minus_iff starfun hypreal_minus hypreal_of_real_def star_of_def star_n_def hypreal_add)
+apply (rule bexI, rule_tac [2] lemma_starrel_refl, clarify) 
 apply (drule_tac x = u in spec, clarify)
 apply (drule_tac x = s in spec, clarify)
 apply (subgoal_tac "\<forall>n::nat. (xa n) \<noteq> x & \<bar>(xa n) + - x\<bar> < s --> \<bar>f (xa n) + - L\<bar> < u")
@@ -270,10 +270,10 @@
 apply (rule ccontr, simp)
 apply (simp add: linorder_not_less)
 apply (drule lemma_skolemize_LIM2, safe)
-apply (drule_tac x = "Abs_hypreal (hyprel``{X})" in spec)
-apply (auto simp add: starfun hypreal_minus hypreal_of_real_def hypreal_add)
+apply (drule_tac x = "Abs_star (starrel``{X})" in spec)
+apply (auto simp add: starfun hypreal_minus hypreal_of_real_def star_of_def star_n_def hypreal_add)
 apply (drule lemma_simp [THEN real_seq_to_hypreal_Infinitesimal])
-apply (simp add: Infinitesimal_FreeUltrafilterNat_iff hypreal_of_real_def hypreal_minus hypreal_add, blast)
+apply (simp add: Infinitesimal_FreeUltrafilterNat_iff hypreal_of_real_def star_of_def star_n_def hypreal_minus hypreal_add, blast)
 apply (drule spec, drule mp, assumption)
 apply (drule FreeUltrafilterNat_all, ultra)
 done
@@ -451,9 +451,9 @@
 apply (rule mem_infmal_iff [THEN iffD2, THEN Infinitesimal_add_approx_self [THEN approx_sym]])
 apply (rule_tac [4] approx_minus_iff2 [THEN iffD1])
  prefer 3 apply (simp add: add_commute)
-apply (rule_tac [2] z = x in eq_Abs_hypreal)
-apply (rule_tac [4] z = x in eq_Abs_hypreal)
-apply (auto simp add: starfun hypreal_of_real_def hypreal_minus hypreal_add add_assoc approx_refl hypreal_zero_def)
+apply (rule_tac [2] z = x in eq_Abs_star)
+apply (rule_tac [4] z = x in eq_Abs_star)
+apply (auto simp add: starfun hypreal_of_real_def star_of_def star_n_def hypreal_minus hypreal_add add_assoc approx_refl hypreal_zero_def)
 done
 
 lemma NSLIM_isCont_iff: "(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)"
@@ -579,10 +579,10 @@
 lemma isUCont_isNSUCont: "isUCont f ==> isNSUCont f"
 apply (simp add: isNSUCont_def isUCont_def approx_def)
 apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, safe)
-apply (rule_tac z = x in eq_Abs_hypreal)
-apply (rule_tac z = y in eq_Abs_hypreal)
+apply (rule_tac z = x in eq_Abs_star)
+apply (rule_tac z = y in eq_Abs_star)
 apply (auto simp add: starfun hypreal_minus hypreal_add)
-apply (rule bexI, rule_tac [2] lemma_hyprel_refl, safe)
+apply (rule bexI, rule_tac [2] lemma_starrel_refl, safe)
 apply (drule_tac x = u in spec, clarify)
 apply (drule_tac x = s in spec, clarify)
 apply (subgoal_tac "\<forall>n::nat. abs ((xa n) + - (xb n)) < s --> abs (f (xa n) + - f (xb n)) < u")
@@ -620,8 +620,8 @@
 apply (rule ccontr, simp)
 apply (simp add: linorder_not_less)
 apply (drule lemma_skolemize_LIM2u, safe)
-apply (drule_tac x = "Abs_hypreal (hyprel``{X})" in spec)
-apply (drule_tac x = "Abs_hypreal (hyprel``{Y})" in spec)
+apply (drule_tac x = "Abs_star (starrel``{X})" in spec)
+apply (drule_tac x = "Abs_star (starrel``{Y})" in spec)
 apply (simp add: starfun hypreal_minus hypreal_add, auto)
 apply (drule lemma_simpu [THEN real_seq_to_hypreal_Infinitesimal2])
 apply (simp add: Infinitesimal_FreeUltrafilterNat_iff hypreal_minus hypreal_add, blast)
diff -r 17256fe71aca -r ad73fb6144cf src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Hyperreal/NSA.thy	Tue Sep 06 23:16:48 2005 +0200
@@ -1774,32 +1774,33 @@
 subsection{*Alternative Definitions for @{term HFinite} using Free Ultrafilter*}
 
 lemma FreeUltrafilterNat_Rep_hypreal:
-     "[| X \<in> Rep_hypreal x; Y \<in> Rep_hypreal x |]
+     "[| X \<in> Rep_star x; Y \<in> Rep_star x |]
       ==> {n. X n = Y n} \<in> FreeUltrafilterNat"
-by (rule_tac z = x in eq_Abs_hypreal, auto, ultra)
+by (rule_tac z = x in eq_Abs_star, auto, ultra)
 
 lemma HFinite_FreeUltrafilterNat:
     "x \<in> HFinite 
-     ==> \<exists>X \<in> Rep_hypreal x. \<exists>u. {n. abs (X n) < u} \<in> FreeUltrafilterNat"
-apply (cases x)
+     ==> \<exists>X \<in> Rep_star x. \<exists>u. {n. abs (X n) < u} \<in> FreeUltrafilterNat"
+apply (rule_tac z = x in eq_Abs_star)
 apply (auto simp add: HFinite_def abs_less_iff minus_less_iff [of x] 
+              star_of_def star_n_def
               hypreal_less SReal_iff hypreal_minus hypreal_of_real_def)
 apply (rule_tac x=x in bexI) 
 apply (rule_tac x=y in exI, auto, ultra)
 done
 
 lemma FreeUltrafilterNat_HFinite:
-     "\<exists>X \<in> Rep_hypreal x.
+     "\<exists>X \<in> Rep_star x.
        \<exists>u. {n. abs (X n) < u} \<in> FreeUltrafilterNat
        ==>  x \<in> HFinite"
-apply (cases x)
+apply (rule_tac z = x in eq_Abs_star)
 apply (auto simp add: HFinite_def abs_less_iff minus_less_iff [of x])
 apply (rule_tac x = "hypreal_of_real u" in bexI)
-apply (auto simp add: hypreal_less SReal_iff hypreal_minus hypreal_of_real_def, ultra+)
+apply (auto simp add: hypreal_less SReal_iff hypreal_minus hypreal_of_real_def star_of_def star_n_def, ultra+)
 done
 
 lemma HFinite_FreeUltrafilterNat_iff:
-     "(x \<in> HFinite) = (\<exists>X \<in> Rep_hypreal x.
+     "(x \<in> HFinite) = (\<exists>X \<in> Rep_star x.
            \<exists>u. {n. abs (X n) < u} \<in> FreeUltrafilterNat)"
 apply (blast intro!: HFinite_FreeUltrafilterNat FreeUltrafilterNat_HFinite)
 done
@@ -1828,7 +1829,7 @@
   ultrafilter for Infinite numbers!
  -------------------------------------*)
 lemma FreeUltrafilterNat_const_Finite:
-     "[| xa: Rep_hypreal x;
+     "[| xa: Rep_star x;
                   {n. abs (xa n) = u} \<in> FreeUltrafilterNat
                |] ==> x \<in> HFinite"
 apply (rule FreeUltrafilterNat_HFinite)
@@ -1838,7 +1839,7 @@
 done
 
 lemma HInfinite_FreeUltrafilterNat:
-     "x \<in> HInfinite ==> \<exists>X \<in> Rep_hypreal x.
+     "x \<in> HInfinite ==> \<exists>X \<in> Rep_star x.
            \<forall>u. {n. u < abs (X n)} \<in> FreeUltrafilterNat"
 apply (frule HInfinite_HFinite_iff [THEN iffD1])
 apply (cut_tac x = x in Rep_hypreal_nonempty)
@@ -1861,7 +1862,7 @@
 by (auto intro: order_less_asym)
 
 lemma FreeUltrafilterNat_HInfinite:
-     "\<exists>X \<in> Rep_hypreal x. \<forall>u.
+     "\<exists>X \<in> Rep_star x. \<forall>u.
                {n. u < abs (X n)} \<in> FreeUltrafilterNat
                ==>  x \<in> HInfinite"
 apply (rule HInfinite_HFinite_iff [THEN iffD2])
@@ -1875,7 +1876,7 @@
 done
 
 lemma HInfinite_FreeUltrafilterNat_iff:
-     "(x \<in> HInfinite) = (\<exists>X \<in> Rep_hypreal x.
+     "(x \<in> HInfinite) = (\<exists>X \<in> Rep_star x.
            \<forall>u. {n. u < abs (X n)} \<in> FreeUltrafilterNat)"
 by (blast intro!: HInfinite_FreeUltrafilterNat FreeUltrafilterNat_HInfinite)
 
@@ -1883,31 +1884,31 @@
 subsection{*Alternative Definitions for @{term Infinitesimal} using Free Ultrafilter*}
 
 lemma Infinitesimal_FreeUltrafilterNat:
-          "x \<in> Infinitesimal ==> \<exists>X \<in> Rep_hypreal x.
+          "x \<in> Infinitesimal ==> \<exists>X \<in> Rep_star x.
            \<forall>u. 0 < u --> {n. abs (X n) < u} \<in> FreeUltrafilterNat"
 apply (simp add: Infinitesimal_def)
 apply (auto simp add: abs_less_iff minus_less_iff [of x])
-apply (cases x)
-apply (auto, rule bexI [OF _ lemma_hyprel_refl], safe)
+apply (rule_tac z = x in eq_Abs_star)
+apply (auto, rule bexI [OF _ lemma_starrel_refl], safe)
 apply (drule hypreal_of_real_less_iff [THEN iffD2])
 apply (drule_tac x = "hypreal_of_real u" in bspec, auto)
-apply (auto simp add: hypreal_less hypreal_minus hypreal_of_real_def, ultra)
+apply (auto simp add: hypreal_less hypreal_minus hypreal_of_real_def star_of_def star_n_def, ultra)
 done
 
 lemma FreeUltrafilterNat_Infinitesimal:
-     "\<exists>X \<in> Rep_hypreal x.
+     "\<exists>X \<in> Rep_star x.
             \<forall>u. 0 < u --> {n. abs (X n) < u} \<in> FreeUltrafilterNat
       ==> x \<in> Infinitesimal"
 apply (simp add: Infinitesimal_def)
-apply (cases x)
+apply (rule_tac z = x in eq_Abs_star)
 apply (auto simp add: abs_less_iff abs_interval_iff minus_less_iff [of x])
 apply (auto simp add: SReal_iff)
 apply (drule_tac [!] x=y in spec) 
-apply (auto simp add: hypreal_less hypreal_minus hypreal_of_real_def, ultra+)
+apply (auto simp add: hypreal_less hypreal_minus hypreal_of_real_def star_of_def star_n_def, ultra+)
 done
 
 lemma Infinitesimal_FreeUltrafilterNat_iff:
-     "(x \<in> Infinitesimal) = (\<exists>X \<in> Rep_hypreal x.
+     "(x \<in> Infinitesimal) = (\<exists>X \<in> Rep_star x.
            \<forall>u. 0 < u --> {n. abs (X n) < u} \<in> FreeUltrafilterNat)"
 apply (blast intro!: Infinitesimal_FreeUltrafilterNat FreeUltrafilterNat_Infinitesimal)
 done
@@ -2008,7 +2009,7 @@
 
 text{*@{term omega} is a member of @{term HInfinite}*}
 
-lemma hypreal_omega: "hyprel``{%n::nat. real (Suc n)} \<in> hypreal"
+lemma hypreal_omega: "starrel``{%n::nat. real (Suc n)} \<in> star"
 by auto
 
 lemma FreeUltrafilterNat_omega: "{n. u < real n} \<in> FreeUltrafilterNat"
@@ -2017,10 +2018,10 @@
 done
 
 theorem HInfinite_omega [simp]: "omega \<in> HInfinite"
-apply (simp add: omega_def)
+apply (simp add: omega_def star_n_def)
 apply (auto intro!: FreeUltrafilterNat_HInfinite)
 apply (rule bexI)
-apply (rule_tac [2] lemma_hyprel_refl, auto)
+apply (rule_tac [2] lemma_starrel_refl, auto)
 apply (simp (no_asm) add: real_of_nat_Suc diff_less_eq [symmetric] FreeUltrafilterNat_omega)
 done
 
@@ -2122,13 +2123,13 @@
  -----------------------------------------------------*)
 lemma real_seq_to_hypreal_Infinitesimal:
      "\<forall>n. abs(X n + -x) < inverse(real(Suc n))
-     ==> Abs_hypreal(hyprel``{X}) + -hypreal_of_real x \<in> Infinitesimal"
-apply (auto intro!: bexI dest: FreeUltrafilterNat_inverse_real_of_posnat FreeUltrafilterNat_all FreeUltrafilterNat_Int intro: order_less_trans FreeUltrafilterNat_subset simp add: hypreal_minus hypreal_of_real_def hypreal_add Infinitesimal_FreeUltrafilterNat_iff hypreal_inverse)
+     ==> Abs_star(starrel``{X}) + -hypreal_of_real x \<in> Infinitesimal"
+apply (auto intro!: bexI dest: FreeUltrafilterNat_inverse_real_of_posnat FreeUltrafilterNat_all FreeUltrafilterNat_Int intro: order_less_trans FreeUltrafilterNat_subset simp add: hypreal_minus hypreal_of_real_def star_of_def star_n_def hypreal_add Infinitesimal_FreeUltrafilterNat_iff hypreal_inverse)
 done
 
 lemma real_seq_to_hypreal_approx:
      "\<forall>n. abs(X n + -x) < inverse(real(Suc n))
-      ==> Abs_hypreal(hyprel``{X}) @= hypreal_of_real x"
+      ==> Abs_star(starrel``{X}) @= hypreal_of_real x"
 apply (subst approx_minus_iff)
 apply (rule mem_infmal_iff [THEN subst])
 apply (erule real_seq_to_hypreal_Infinitesimal)
@@ -2136,14 +2137,14 @@
 
 lemma real_seq_to_hypreal_approx2:
      "\<forall>n. abs(x + -X n) < inverse(real(Suc n))
-               ==> Abs_hypreal(hyprel``{X}) @= hypreal_of_real x"
+               ==> Abs_star(starrel``{X}) @= hypreal_of_real x"
 apply (simp add: abs_minus_add_cancel real_seq_to_hypreal_approx)
 done
 
 lemma real_seq_to_hypreal_Infinitesimal2:
      "\<forall>n. abs(X n + -Y n) < inverse(real(Suc n))
-      ==> Abs_hypreal(hyprel``{X}) +
-          -Abs_hypreal(hyprel``{Y}) \<in> Infinitesimal"
+      ==> Abs_star(starrel``{X}) +
+          -Abs_star(starrel``{Y}) \<in> Infinitesimal"
 by (auto intro!: bexI
 	 dest: FreeUltrafilterNat_inverse_real_of_posnat 
 	       FreeUltrafilterNat_all FreeUltrafilterNat_Int
diff -r 17256fe71aca -r ad73fb6144cf src/HOL/Hyperreal/NatStar.thy
--- a/src/HOL/Hyperreal/NatStar.thy	Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Hyperreal/NatStar.thy	Tue Sep 06 23:16:48 2005 +0200
@@ -33,12 +33,12 @@
 
     starfunNat :: "(nat => real) => hypnat => hypreal"
                   ("*fNat* _" [80] 80)
-    "*fNat* f  == (%x. Abs_hypreal(\<Union>X\<in>Rep_hypnat(x). hyprel``{%n. f (X n)}))"
+    "*fNat* f  == (%x. Abs_star(\<Union>X\<in>Rep_hypnat(x). starrel``{%n. f (X n)}))"
 
    starfunNat_n :: "(nat => (nat => real)) => hypnat => hypreal"
                    ("*fNatn* _" [80] 80)
     "*fNatn* F ==
-      (%x. Abs_hypreal(\<Union>X\<in>Rep_hypnat(x). hyprel``{%n. (F n)(X n)}))"
+      (%x. Abs_star(\<Union>X\<in>Rep_hypnat(x). starrel``{%n. (F n)(X n)}))"
 
    InternalNatFuns :: "(hypnat => hypreal) set"
     "InternalNatFuns == {X. \<exists>F. X = *fNatn* F}"
@@ -194,9 +194,9 @@
 (* f::nat=>real *)
 lemma starfunNat:
       "( *fNat* f) (Abs_hypnat(hypnatrel``{%n. X n})) =
-       Abs_hypreal(hyprel `` {%n. f (X n)})"
+       Abs_star(starrel `` {%n. f (X n)})"
 apply (simp add: starfunNat_def)
-apply (rule arg_cong [where f = Abs_hypreal])
+apply (rule arg_cong [where f = Abs_star])
 apply (auto, ultra)
 done
 
@@ -287,7 +287,7 @@
 
 lemma starfunNat_const_fun [simp]: "( *fNat* (%x. k)) z = hypreal_of_real k"
 apply (cases z)
-apply (simp add: starfunNat hypreal_of_real_def)
+apply (simp add: starfunNat hypreal_of_real_def star_of_def star_n_def)
 done
 
 lemma starfunNat2_const_fun [simp]: "( *fNat2* (%x. k)) z = hypnat_of_nat  k"
@@ -312,7 +312,7 @@
 
 lemma starfunNat_eq [simp]:
      "( *fNat* f) (hypnat_of_nat a) = hypreal_of_real (f a)"
-by (simp add: starfunNat hypnat_of_nat_eq hypreal_of_real_def)
+by (simp add: starfunNat hypnat_of_nat_eq hypreal_of_real_def star_of_def star_n_def)
 
 lemma starfunNat2_eq [simp]:
      "( *fNat2* f) (hypnat_of_nat a) = hypnat_of_nat (f a)"
@@ -362,7 +362,7 @@
 
 lemma starfunNat_pow: "( *fNat* (%n. r ^ n)) N = (hypreal_of_real r) pow N"
 apply (cases N)
-apply (simp add: hyperpow hypreal_of_real_def starfunNat)
+apply (simp add: hyperpow hypreal_of_real_def star_of_def star_n_def starfunNat)
 done
 
 lemma starfunNat_pow2:
@@ -372,7 +372,7 @@
 done
 
 lemma starfun_pow: "( *f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n"
-apply (rule_tac z = R in eq_Abs_hypreal)
+apply (rule_tac z = R in eq_Abs_star)
 apply (simp add: hyperpow starfun hypnat_of_nat_eq)
 done
 
@@ -401,9 +401,9 @@
 
 lemma starfunNat_n:
      "( *fNatn* f) (Abs_hypnat(hypnatrel``{%n. X n})) =
-      Abs_hypreal(hyprel `` {%n. f n (X n)})"
+      Abs_star(starrel `` {%n. f n (X n)})"
 apply (simp add: starfunNat_n_def)
-apply (rule_tac f = Abs_hypreal in arg_cong, auto, ultra)
+apply (rule_tac f = Abs_star in arg_cong, auto, ultra)
 done
 
 text{*Multiplication: @{text "( *fn) x ( *gn) = *(fn x gn)"}*}
@@ -436,7 +436,7 @@
 lemma starfunNat_n_const_fun [simp]:
      "( *fNatn* (%i x. k)) z = hypreal_of_real  k"
 apply (cases z)
-apply (simp add: starfunNat_n hypreal_of_real_def)
+apply (simp add: starfunNat_n hypreal_of_real_def star_of_def star_n_def)
 done
 
 lemma starfunNat_n_minus: "- ( *fNatn* f) x = ( *fNatn* (%i x. - (f i) x)) x"
@@ -445,7 +445,7 @@
 done
 
 lemma starfunNat_n_eq [simp]:
-     "( *fNatn* f) (hypnat_of_nat n) = Abs_hypreal(hyprel `` {%i. f i n})"
+     "( *fNatn* f) (hypnat_of_nat n) = Abs_star(starrel `` {%i. f i n})"
 by (simp add: starfunNat_n hypnat_of_nat_eq)
 
 lemma starfun_eq_iff: "(( *fNat* f) = ( *fNat* g)) = (f = g)"
diff -r 17256fe71aca -r ad73fb6144cf src/HOL/Hyperreal/SEQ.thy
--- a/src/HOL/Hyperreal/SEQ.thy	Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy	Tue Sep 06 23:16:48 2005 +0200
@@ -70,7 +70,7 @@
 lemma SEQ_Infinitesimal:
       "( *fNat* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal"
 apply (simp add: hypnat_omega_def Infinitesimal_FreeUltrafilterNat_iff starfunNat)
-apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
+apply (rule bexI, rule_tac [2] lemma_starrel_refl)
 apply (simp add: real_of_nat_Suc_gt_zero FreeUltrafilterNat_inverse_real_of_posnat)
 done
 
@@ -95,8 +95,9 @@
 apply (rule_tac z = N in eq_Abs_hypnat)
 apply (rule approx_minus_iff [THEN iffD2])
 apply (auto simp add: starfunNat mem_infmal_iff [symmetric] hypreal_of_real_def
+              star_of_def star_n_def
               hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff)
-apply (rule bexI [OF _ lemma_hyprel_refl], safe)
+apply (rule bexI [OF _ lemma_starrel_refl], safe)
 apply (drule_tac x = u in spec, safe)
 apply (drule_tac x = no in spec, fuf)
 apply (blast dest: less_imp_le)
@@ -162,7 +163,7 @@
 lemma lemmaLIM3: "[| 0 < r; \<forall>n. r \<le> \<bar>X (f n) + - L\<bar>;
            ( *fNat* X) (Abs_hypnat (hypnatrel `` {f})) +
            - hypreal_of_real  L \<approx> 0 |] ==> False"
-apply (auto simp add: starfunNat mem_infmal_iff [symmetric] hypreal_of_real_def hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff)
+apply (auto simp add: starfunNat mem_infmal_iff [symmetric] hypreal_of_real_def star_of_def star_n_def hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff)
 apply (rename_tac "Y")
 apply (drule_tac x = r in spec, safe)
 apply (drule FreeUltrafilterNat_Int, assumption)
@@ -506,7 +507,7 @@
 apply (rule_tac z = N in eq_Abs_hypnat)
 apply (auto simp add: starfunNat HFinite_FreeUltrafilterNat_iff 
                       HNatInfinite_FreeUltrafilterNat_iff)
-apply (rule bexI [OF _ lemma_hyprel_refl]) 
+apply (rule bexI [OF _ lemma_starrel_refl]) 
 apply (drule_tac f = Xa in lemma_Bseq)
 apply (rule_tac x = "K+1" in exI)
 apply (drule_tac P="%n. ?f n \<le> K" in FreeUltrafilterNat_all, ultra)
@@ -537,9 +538,9 @@
 
 lemma real_seq_to_hypreal_HInfinite:
      "\<forall>N. real(Suc N) < \<bar>X (f N)\<bar>
-      ==>  Abs_hypreal(hyprel``{X o f}) : HInfinite"
+      ==>  Abs_star(starrel``{X o f}) : HInfinite"
 apply (auto simp add: HInfinite_FreeUltrafilterNat_iff o_def)
-apply (rule bexI [OF _ lemma_hyprel_refl], clarify)  
+apply (rule bexI [OF _ lemma_starrel_refl], clarify)  
 apply (cut_tac u = u in FreeUltrafilterNat_nat_gt_real)
 apply (drule FreeUltrafilterNat_all)
 apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset])
@@ -1163,15 +1164,15 @@
 subsection{*Hyperreals and Sequences*}
 
 text{*A bounded sequence is a finite hyperreal*}
-lemma NSBseq_HFinite_hypreal: "NSBseq X ==> Abs_hypreal(hyprel``{X}) : HFinite"
-by (auto intro!: bexI lemma_hyprel_refl 
+lemma NSBseq_HFinite_hypreal: "NSBseq X ==> Abs_star(starrel``{X}) : HFinite"
+by (auto intro!: bexI lemma_starrel_refl 
             intro: FreeUltrafilterNat_all [THEN FreeUltrafilterNat_subset]
             simp add: HFinite_FreeUltrafilterNat_iff Bseq_NSBseq_iff [symmetric]
                       Bseq_iff1a)
 
 text{*A sequence converging to zero defines an infinitesimal*}
 lemma NSLIMSEQ_zero_Infinitesimal_hypreal:
-      "X ----NS> 0 ==> Abs_hypreal(hyprel``{X}) : Infinitesimal"
+      "X ----NS> 0 ==> Abs_star(starrel``{X}) : Infinitesimal"
 apply (simp add: NSLIMSEQ_def)
 apply (drule_tac x = whn in bspec)
 apply (simp add: HNatInfinite_whn)
diff -r 17256fe71aca -r ad73fb6144cf src/HOL/Hyperreal/Star.thy
--- a/src/HOL/Hyperreal/Star.thy	Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Hyperreal/Star.thy	Tue Sep 06 23:16:48 2005 +0200
@@ -13,27 +13,27 @@
 constdefs
     (* nonstandard extension of sets *)
     starset :: "real set => hypreal set"          ("*s* _" [80] 80)
-    "*s* A  == {x. \<forall>X \<in> Rep_hypreal(x). {n::nat. X n  \<in> A}: FreeUltrafilterNat}"
+    "*s* A  == {x. \<forall>X \<in> Rep_star(x). {n::nat. X n  \<in> A}: FreeUltrafilterNat}"
 
     (* internal sets *)
     starset_n :: "(nat => real set) => hypreal set"        ("*sn* _" [80] 80)
-    "*sn* As  == {x. \<forall>X \<in> Rep_hypreal(x). {n::nat. X n : (As n)}: FreeUltrafilterNat}"
+    "*sn* As  == {x. \<forall>X \<in> Rep_star(x). {n::nat. X n : (As n)}: FreeUltrafilterNat}"
 
     InternalSets :: "hypreal set set"
     "InternalSets == {X. \<exists>As. X = *sn* As}"
 
     (* nonstandard extension of function *)
     is_starext  :: "[hypreal => hypreal, real => real] => bool"
-    "is_starext F f == (\<forall>x y. \<exists>X \<in> Rep_hypreal(x). \<exists>Y \<in> Rep_hypreal(y).
+    "is_starext F f == (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y).
                         ((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))"
 
     starfun :: "(real => real) => hypreal => hypreal"       ("*f* _" [80] 80)
-    "*f* f  == (%x. Abs_hypreal(\<Union>X \<in> Rep_hypreal(x). hyprel``{%n. f(X n)}))"
+    "*f* f  == (%x. Abs_star(\<Union>X \<in> Rep_star(x). starrel``{%n. f(X n)}))"
 
     (* internal functions *)
     starfun_n :: "(nat => (real => real)) => hypreal => hypreal"
                  ("*fn* _" [80] 80)
-    "*fn* F  == (%x. Abs_hypreal(\<Union>X \<in> Rep_hypreal(x). hyprel``{%n. (F n)(X n)}))"
+    "*fn* F  == (%x. Abs_star(\<Union>X \<in> Rep_star(x). starrel``{%n. (F n)(X n)}))"
 
     InternalFuns :: "(hypreal => hypreal) set"
     "InternalFuns == {X. \<exists>F. X = *fn* F}"
@@ -69,7 +69,7 @@
  prefer 2 apply (blast intro: FreeUltrafilterNat_subset)
 apply (drule FreeUltrafilterNat_Compl_mem)
 apply (drule bspec, assumption)
-apply (rule_tac z = x in eq_Abs_hypreal, auto, ultra)
+apply (rule_tac z = x in eq_Abs_star, auto, ultra)
 done
 
 lemma STAR_Int: "*s* (A Int B) = *s* A Int *s* B"
@@ -80,7 +80,7 @@
 
 lemma STAR_Compl: "*s* -A = -( *s* A)"
 apply (auto simp add: starset_def)
-apply (rule_tac [!] z = x in eq_Abs_hypreal)
+apply (rule_tac [!] z = x in eq_Abs_star)
 apply (auto dest!: bspec, ultra)
 apply (drule FreeUltrafilterNat_Compl_mem, ultra)
 done
@@ -97,23 +97,23 @@
 done
 
 lemma STAR_mem: "a  \<in> A ==> hypreal_of_real a : *s* A"
-apply (simp add: starset_def hypreal_of_real_def)
+apply (simp add: starset_def hypreal_of_real_def star_of_def star_n_def)
 apply (auto intro: FreeUltrafilterNat_subset)
 done
 
 lemma STAR_hypreal_of_real_image_subset: "hypreal_of_real ` A <= *s* A"
 apply (simp add: starset_def)
-apply (auto simp add: hypreal_of_real_def)
+apply (auto simp add: hypreal_of_real_def star_of_def star_n_def)
 apply (blast intro: FreeUltrafilterNat_subset)
 done
 
 lemma STAR_hypreal_of_real_Int: "*s* X Int Reals = hypreal_of_real ` X"
 apply (simp add: starset_def)
-apply (auto simp add: hypreal_of_real_def SReal_def)
-apply (simp add: hypreal_of_real_def [symmetric])
+apply (auto simp add: hypreal_of_real_def star_of_def star_n_def SReal_def)
+apply (fold star_n_def star_of_def hypreal_of_real_def)
 apply (rule imageI, rule ccontr)
 apply (drule bspec)
-apply (rule lemma_hyprel_refl)
+apply (rule lemma_starrel_refl)
 prefer 2 apply (blast intro: FreeUltrafilterNat_subset, auto)
 done
 
@@ -125,22 +125,22 @@
 
 lemma STAR_real_seq_to_hypreal:
     "\<forall>n. (X n) \<notin> M
-          ==> Abs_hypreal(hyprel``{X}) \<notin> *s* M"
+          ==> Abs_star(starrel``{X}) \<notin> *s* M"
 apply (simp add: starset_def)
-apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
+apply (rule bexI, rule_tac [2] lemma_starrel_refl, auto)
 done
 
 lemma STAR_singleton: "*s* {x} = {hypreal_of_real x}"
 apply (simp add: starset_def)
-apply (auto simp add: hypreal_of_real_def)
-apply (rule_tac z = xa in eq_Abs_hypreal)
+apply (auto simp add: hypreal_of_real_def star_of_def star_n_def)
+apply (rule_tac z = xa in eq_Abs_star)
 apply (auto intro: FreeUltrafilterNat_subset)
 done
 declare STAR_singleton [simp]
 
 lemma STAR_not_mem: "x \<notin> F ==> hypreal_of_real x \<notin> *s* F"
-apply (auto simp add: starset_def hypreal_of_real_def)
-apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
+apply (auto simp add: starset_def hypreal_of_real_def star_of_def star_n_def)
+apply (rule bexI, rule_tac [2] lemma_starrel_refl, auto)
 done
 
 lemma STAR_subset_closed: "[| x : *s* A; A <= B |] ==> x : *s* B"
@@ -176,49 +176,49 @@
 
 lemma hrabs_is_starext_rabs: "is_starext abs abs"
 apply (simp add: is_starext_def, safe)
-apply (rule_tac z = x in eq_Abs_hypreal)
-apply (rule_tac z = y in eq_Abs_hypreal, auto)
-apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
-apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
+apply (rule_tac z = x in eq_Abs_star)
+apply (rule_tac z = y in eq_Abs_star, auto)
+apply (rule bexI, rule_tac [2] lemma_starrel_refl)
+apply (rule bexI, rule_tac [2] lemma_starrel_refl)
 apply (auto dest!: spec 
             simp add: hypreal_minus abs_if hypreal_zero_def
                   hypreal_le hypreal_less)
 apply (arith | ultra)+
 done
 
-lemma Rep_hypreal_FreeUltrafilterNat:
-     "[| X \<in> Rep_hypreal z; Y \<in> Rep_hypreal z |]
+lemma Rep_star_FreeUltrafilterNat:
+     "[| X \<in> Rep_star z; Y \<in> Rep_star z |]
       ==> {n. X n = Y n} : FreeUltrafilterNat"
-apply (cases z)
+apply (rule_tac z = z in eq_Abs_star)
 apply (auto, ultra)
 done
 
 text{*Nonstandard extension of functions*}
 
-lemma starfun_congruent: "(%X. hyprel``{%n. f (X n)}) respects hyprel"
+lemma starfun_congruent: "(%X. starrel``{%n. f (X n)}) respects starrel"
 by (simp add: congruent_def, auto, ultra)
 
 lemma starfun:
-      "( *f* f) (Abs_hypreal(hyprel``{%n. X n})) =
-       Abs_hypreal(hyprel `` {%n. f (X n)})"
+      "( *f* f) (Abs_star(starrel``{%n. X n})) =
+       Abs_star(starrel `` {%n. f (X n)})"
 apply (simp add: starfun_def)
-apply (rule_tac f = Abs_hypreal in arg_cong)
-apply (simp add: hyprel_in_hypreal [THEN Abs_hypreal_inverse] 
-                 UN_equiv_class [OF equiv_hyprel starfun_congruent])
+apply (rule_tac f = Abs_star in arg_cong)
+apply (simp add: starrel_in_hypreal [THEN Abs_star_inverse] 
+                 UN_equiv_class [OF equiv_starrel starfun_congruent])
 done
 
 lemma starfun_if_eq:
      "w \<noteq> hypreal_of_real x
        ==> ( *f* (\<lambda>z. if z = x then a else g z)) w = ( *f* g) w" 
-apply (cases w) 
-apply (simp add: hypreal_of_real_def starfun, ultra)
+apply (rule_tac z = w in eq_Abs_star)
+apply (simp add: hypreal_of_real_def star_of_def star_n_def starfun, ultra)
 done
 
 (*-------------------------------------------
   multiplication: ( *f) x ( *g) = *(f x g)
  ------------------------------------------*)
 lemma starfun_mult: "( *f* f) xa * ( *f* g) xa = ( *f* (%x. f x * g x)) xa"
-by (cases xa, simp add: starfun hypreal_mult)
+by (rule_tac z = xa in eq_Abs_star, simp add: starfun hypreal_mult)
 
 declare starfun_mult [symmetric, simp]
 
@@ -226,7 +226,7 @@
   addition: ( *f) + ( *g) = *(f + g)
  ---------------------------------------*)
 lemma starfun_add: "( *f* f) xa + ( *f* g) xa = ( *f* (%x. f x + g x)) xa"
-by (cases xa, simp add: starfun hypreal_add)
+by (rule_tac z = xa in eq_Abs_star, simp add: starfun hypreal_add)
 declare starfun_add [symmetric, simp]
 
 (*--------------------------------------------
@@ -234,7 +234,7 @@
  -------------------------------------------*)
 
 lemma starfun_minus: "- ( *f* f) x = ( *f* (%x. - f x)) x"
-apply (cases x)
+apply (rule_tac z = x in eq_Abs_star)
 apply (auto simp add: starfun hypreal_minus)
 done
 declare starfun_minus [symmetric, simp]
@@ -257,7 +257,7 @@
 
 lemma starfun_o2: "(%x. ( *f* f) (( *f* g) x)) = *f* (%x. f (g x))"
 apply (rule ext)
-apply (rule_tac z = x in eq_Abs_hypreal)
+apply (rule_tac z = x in eq_Abs_star)
 apply (auto simp add: starfun)
 done
 
@@ -268,8 +268,8 @@
 
 text{*NS extension of constant function*}
 lemma starfun_const_fun: "( *f* (%x. k)) xa = hypreal_of_real  k"
-apply (cases xa)
-apply (auto simp add: starfun hypreal_of_real_def)
+apply (rule_tac z = xa in eq_Abs_star)
+apply (auto simp add: starfun hypreal_of_real_def star_of_def star_n_def)
 done
 
 declare starfun_const_fun [simp]
@@ -277,12 +277,12 @@
 text{*the NS extension of the identity function*}
 
 lemma starfun_Idfun_approx: "x @= hypreal_of_real a ==> ( *f* (%x. x)) x @= hypreal_of_real  a"
-apply (cases x)
+apply (rule_tac z = x in eq_Abs_star)
 apply (auto simp add: starfun)
 done
 
 lemma starfun_Id: "( *f* (%x. x)) x = x"
-apply (cases x)
+apply (rule_tac z = x in eq_Abs_star)
 apply (auto simp add: starfun)
 done
 declare starfun_Id [simp]
@@ -291,8 +291,8 @@
 
 lemma is_starext_starfun: "is_starext ( *f* f) f"
 apply (simp add: is_starext_def, auto)
-apply (rule_tac z = x in eq_Abs_hypreal)
-apply (rule_tac z = y in eq_Abs_hypreal)
+apply (rule_tac z = x in eq_Abs_star)
+apply (rule_tac z = y in eq_Abs_star)
 apply (auto intro!: bexI simp add: starfun)
 done
 
@@ -301,7 +301,7 @@
 lemma is_starfun_starext: "is_starext F f ==> F = *f* f"
 apply (simp add: is_starext_def)
 apply (rule ext)
-apply (rule_tac z = x in eq_Abs_hypreal)
+apply (rule_tac z = x in eq_Abs_star)
 apply (drule_tac x = x in spec)
 apply (drule_tac x = "( *f* f) x" in spec)
 apply (auto dest!: FreeUltrafilterNat_Compl_mem simp add: starfun, ultra)
@@ -314,7 +314,7 @@
    version for real arguments. i.e they are the same
    for all real arguments*}
 lemma starfun_eq: "( *f* f) (hypreal_of_real a) = hypreal_of_real (f a)"
-by (auto simp add: starfun hypreal_of_real_def)
+by (auto simp add: starfun hypreal_of_real_def star_of_def star_n_def)
 
 declare starfun_eq [simp]
 
@@ -323,13 +323,13 @@
 
 (* useful for NS definition of derivatives *)
 lemma starfun_lambda_cancel: "( *f* (%h. f (x + h))) xa  = ( *f* f) (hypreal_of_real  x + xa)"
-apply (cases xa)
-apply (auto simp add: starfun hypreal_of_real_def hypreal_add)
+apply (rule_tac z = xa in eq_Abs_star)
+apply (auto simp add: starfun hypreal_of_real_def star_of_def star_n_def hypreal_add)
 done
 
 lemma starfun_lambda_cancel2: "( *f* (%h. f(g(x + h)))) xa = ( *f* (f o g)) (hypreal_of_real x + xa)"
-apply (cases xa)
-apply (auto simp add: starfun hypreal_of_real_def hypreal_add)
+apply (rule_tac z = xa in eq_Abs_star)
+apply (auto simp add: starfun hypreal_of_real_def star_of_def star_n_def hypreal_add)
 done
 
 lemma starfun_mult_HFinite_approx: "[| ( *f* f) xa @= l; ( *f* g) xa @= m;
@@ -355,13 +355,13 @@
 by (rule hrabs_is_starext_rabs [THEN is_starext_starfun_iff [THEN iffD1], symmetric])
 
 lemma starfun_inverse_inverse: "( *f* inverse) x = inverse(x)"
-apply (cases x)
+apply (rule_tac z = x in eq_Abs_star)
 apply (auto simp add: starfun hypreal_inverse hypreal_zero_def)
 done
 declare starfun_inverse_inverse [simp]
 
 lemma starfun_inverse: "inverse (( *f* f) x) = ( *f* (%x. inverse (f x))) x"
-apply (cases x)
+apply (rule_tac z = x in eq_Abs_star)
 apply (auto simp add: starfun hypreal_inverse)
 done
 declare starfun_inverse [symmetric, simp]
@@ -371,7 +371,7 @@
 declare starfun_divide [symmetric, simp]
 
 lemma starfun_inverse2: "inverse (( *f* f) x) = ( *f* (%x. inverse (f x))) x"
-apply (cases x)
+apply (rule_tac z = x in eq_Abs_star)
 apply (auto intro: FreeUltrafilterNat_subset dest!: FreeUltrafilterNat_Compl_mem simp add: starfun hypreal_inverse hypreal_zero_def)
 done
 
@@ -380,7 +380,7 @@
 lemma starfun_mem_starset:
       "( *f* f) x : *s* A ==> x : *s* {x. f x  \<in> A}"
 apply (simp add: starset_def)
-apply (cases x)
+apply (rule_tac z = x in eq_Abs_star)
 apply (auto simp add: starfun)
 apply (rename_tac "X")
 apply (drule_tac x = "%n. f (X n) " in bspec)
@@ -391,8 +391,8 @@
    applied entrywise to equivalence class representative.
    This is easily proved using starfun and ns extension thm*}
 lemma hypreal_hrabs:
-     "abs (Abs_hypreal (hyprel``{X})) = Abs_hypreal(hyprel `` {%n. abs (X n)})"
-by (simp add: starfun_rabs_hrabs [symmetric] starfun)
+     "abs (Abs_star (starrel``{X})) = Abs_star(starrel `` {%n. abs (X n)})"
+by (rule hypreal_hrabs)
 
 text{*nonstandard extension of set through nonstandard extension
    of rabs function i.e hrabs. A more general result should be
@@ -402,9 +402,10 @@
    "*s* {x. abs (x + - y) < r} =
      {x. abs(x + -hypreal_of_real y) < hypreal_of_real r}"
 apply (simp add: starset_def, safe)
-apply (rule_tac [!] z = x in eq_Abs_hypreal)
+apply (rule_tac [!] z = x in eq_Abs_star)
 apply (auto intro!: exI dest!: bspec
-             simp add: hypreal_minus hypreal_of_real_def hypreal_add 
+             simp add: hypreal_minus hypreal_of_real_def hypreal_add
+                       star_of_def star_n_def 
                        hypreal_hrabs hypreal_less)
 apply ultra
 done
@@ -413,9 +414,10 @@
   "*s* {x. abs (f x + - y) < r} =
        {x. abs(( *f* f) x + -hypreal_of_real y) < hypreal_of_real r}"
 apply (simp add: starset_def, safe)
-apply (rule_tac [!] z = x in eq_Abs_hypreal)
+apply (rule_tac [!] z = x in eq_Abs_star)
 apply (auto intro!: exI dest!: bspec
              simp add: hypreal_minus hypreal_of_real_def hypreal_add
+                       star_of_def star_n_def
                        hypreal_hrabs hypreal_less starfun)
 apply ultra
 done
@@ -425,17 +427,18 @@
    move both theorems??*}
 lemma Infinitesimal_FreeUltrafilterNat_iff2:
      "(x \<in> Infinitesimal) =
-      (\<exists>X \<in> Rep_hypreal(x).
+      (\<exists>X \<in> Rep_star(x).
         \<forall>m. {n. abs(X n) < inverse(real(Suc m))}
                 \<in>  FreeUltrafilterNat)"
-apply (cases x)
-apply (auto intro!: bexI lemma_hyprel_refl 
+apply (rule_tac z = x in eq_Abs_star)
+apply (auto intro!: bexI lemma_starrel_refl 
             simp add: Infinitesimal_hypreal_of_nat_iff hypreal_of_real_def
+     star_of_def star_n_def
      hypreal_inverse hypreal_hrabs hypreal_less hypreal_of_nat_eq)
 apply (drule_tac x = n in spec, ultra)
 done
 
-lemma approx_FreeUltrafilterNat_iff: "(Abs_hypreal(hyprel``{X}) @= Abs_hypreal(hyprel``{Y})) =
+lemma approx_FreeUltrafilterNat_iff: "(Abs_star(starrel``{X}) @= Abs_star(starrel``{Y})) =
       (\<forall>m. {n. abs (X n + - Y n) <
                   inverse(real(Suc m))} : FreeUltrafilterNat)"
 apply (subst approx_minus_iff)
@@ -447,7 +450,7 @@
 lemma inj_starfun: "inj starfun"
 apply (rule inj_onI)
 apply (rule ext, rule ccontr)
-apply (drule_tac x = "Abs_hypreal (hyprel ``{%n. xa}) " in fun_cong)
+apply (drule_tac x = "Abs_star (starrel ``{%n. xa}) " in fun_cong)
 apply (auto simp add: starfun)
 done
 
@@ -480,7 +483,7 @@
 val starset_n_starset = thm "starset_n_starset";
 val starfun_n_starfun = thm "starfun_n_starfun";
 val hrabs_is_starext_rabs = thm "hrabs_is_starext_rabs";
-val Rep_hypreal_FreeUltrafilterNat = thm "Rep_hypreal_FreeUltrafilterNat";
+val Rep_star_FreeUltrafilterNat = thm "Rep_star_FreeUltrafilterNat";
 val starfun_congruent = thm "starfun_congruent";
 val starfun = thm "starfun";
 val starfun_mult = thm "starfun_mult";
diff -r 17256fe71aca -r ad73fb6144cf src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Tue Sep 06 23:16:48 2005 +0200
@@ -2473,7 +2473,7 @@
 by (erule DERIV_fun_exp)
 
 lemma STAR_exp_ln: "0 < z ==> ( *f* (%x. exp (ln x))) z = z"
-apply (rule_tac z = z in eq_Abs_hypreal)
+apply (rule_tac z = z in eq_Abs_star)
 apply (auto simp add: starfun hypreal_zero_def hypreal_less)
 done
 
diff -r 17256fe71aca -r ad73fb6144cf src/HOL/Hyperreal/fuf.ML
--- a/src/HOL/Hyperreal/fuf.ML	Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Hyperreal/fuf.ML	Tue Sep 06 23:16:48 2005 +0200
@@ -22,10 +22,10 @@
 |   get_fuf_hyps (x::xs) zs =
         case (concl_of x) of
         (_ $ (Const ("Not",_) $ (Const ("op :",_) $ _ $
-             Const ("HyperDef.FreeUltrafilterNat",_)))) =>  get_fuf_hyps xs
+             Const ("StarType.FreeUltrafilterNat",_)))) =>  get_fuf_hyps xs
                                               ((x RS FreeUltrafilterNat_Compl_mem)::zs)
        |(_ $ (Const ("op :",_) $ _ $
-             Const ("HyperDef.FreeUltrafilterNat",_)))  =>  get_fuf_hyps xs (x::zs)
+             Const ("StarType.FreeUltrafilterNat",_)))  =>  get_fuf_hyps xs (x::zs)
        | _ => get_fuf_hyps xs zs;
 
 fun inter_prems [] = raise FUFempty