diff -r 66da6af2b0c9 -r 9edd495b6330 src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Tue Dec 12 07:13:06 2006 +0100
+++ b/src/HOL/Hyperreal/HyperDef.thy	Tue Dec 12 07:46:40 2006 +0100
@@ -19,12 +19,14 @@
   "hypreal_of_real == star_of"
 
 definition
-  omega :: hypreal where   -- {*an infinite number @{text "= [<1,2,3,...>]"} *}
-  "omega = star_n (%n. real (Suc n))"
+  omega :: hypreal where
+   -- {*an infinite number @{text "= [<1,2,3,...>]"} *}
+  "omega = star_n (\<lambda>n. real (Suc n))"
 
 definition
-  epsilon :: hypreal where   -- {*an infinitesimal number @{text "= [<1,1/2,1/3,...>]"} *}
-  "epsilon = star_n (%n. inverse (real (Suc n)))"
+  epsilon :: hypreal where
+   -- {*an infinitesimal number @{text "= [<1,1/2,1/3,...>]"} *}
+  "epsilon = star_n (\<lambda>n. inverse (real (Suc n)))"
 
 notation (xsymbols)
   omega  ("\<omega>") and
@@ -42,31 +44,31 @@
 defs (overloaded)
   star_scaleR_def [transfer_unfold]: "scaleR r \<equiv> *f* (scaleR r)"
 
-lemma Standard_scaleR [simp]: "x \<in> Standard \<Longrightarrow> r *# x \<in> Standard"
+lemma Standard_scaleR [simp]: "x \<in> Standard \<Longrightarrow> scaleR r x \<in> Standard"
 by (simp add: star_scaleR_def)
 
-lemma star_of_scaleR [simp]: "star_of (r *# x) = r *# star_of x"
+lemma star_of_scaleR [simp]: "star_of (scaleR r x) = scaleR r (star_of x)"
 by transfer (rule refl)
 
 instance star :: (real_vector) real_vector
 proof
   fix a b :: real
-  show "\<And>x y::'a star. a *# (x + y) = a *# x + a *# y"
+  show "\<And>x y::'a star. scaleR a (x + y) = scaleR a x + scaleR a y"
     by transfer (rule scaleR_right_distrib)
-  show "\<And>x::'a star. (a + b) *# x = a *# x + b *# x"
+  show "\<And>x::'a star. scaleR (a + b) x = scaleR a x + scaleR b x"
     by transfer (rule scaleR_left_distrib)
-  show "\<And>x::'a star. a *# b *# x = (a * b) *# x"
+  show "\<And>x::'a star. scaleR a (scaleR b x) = scaleR (a * b) x"
     by transfer (rule scaleR_scaleR)
-  show "\<And>x::'a star. 1 *# x = x"
+  show "\<And>x::'a star. scaleR 1 x = x"
     by transfer (rule scaleR_one)
 qed
 
 instance star :: (real_algebra) real_algebra
 proof
   fix a :: real
-  show "\<And>x y::'a star. a *# x * y = a *# (x * y)"
+  show "\<And>x y::'a star. scaleR a x * y = scaleR a (x * y)"
     by transfer (rule mult_scaleR_left)
-  show "\<And>x y::'a star. x * a *# y = a *# (x * y)"
+  show "\<And>x y::'a star. x * scaleR a y = scaleR a (x * y)"
     by transfer (rule mult_scaleR_right)
 qed
 
@@ -117,52 +119,47 @@
 by (rule FreeUltrafilterNat_mem [THEN freeultrafilter.filter])
 
 lemma FreeUltrafilterNat_finite: "finite x ==> x \<notin> FreeUltrafilterNat"
-by (rule FreeUltrafilterNat_mem [THEN freeultrafilter.finite])
+by (rule FreeUltrafilterNat.finite)
 
 lemma FreeUltrafilterNat_not_finite: "x \<in> FreeUltrafilterNat ==> ~ finite x"
-thm FreeUltrafilterNat_mem
-thm freeultrafilter.infinite
-thm FreeUltrafilterNat_mem [THEN freeultrafilter.infinite]
-by (rule FreeUltrafilterNat_mem [THEN freeultrafilter.infinite])
+by (rule FreeUltrafilterNat.infinite)
 
-lemma FreeUltrafilterNat_empty [simp]: "{} \<notin> FreeUltrafilterNat"
-by (rule FilterNat_mem [THEN filter.empty])
+lemma FreeUltrafilterNat_empty: "{} \<notin> FreeUltrafilterNat"
+by (rule FreeUltrafilterNat.empty)
 
 lemma FreeUltrafilterNat_Int:
      "[| X \<in> FreeUltrafilterNat;  Y \<in> FreeUltrafilterNat |]   
       ==> X Int Y \<in> FreeUltrafilterNat"
-by (rule FilterNat_mem [THEN filter.Int])
+by (rule FreeUltrafilterNat.Int)
 
 lemma FreeUltrafilterNat_subset:
      "[| X \<in> FreeUltrafilterNat;  X \<subseteq> Y |]  
       ==> Y \<in> FreeUltrafilterNat"
-by (rule FilterNat_mem [THEN filter.subset])
+by (rule FreeUltrafilterNat.subset)
 
 lemma FreeUltrafilterNat_Compl:
      "X \<in> FreeUltrafilterNat ==> -X \<notin> FreeUltrafilterNat"
-apply (erule contrapos_pn)
-apply (erule UltrafilterNat_mem [THEN ultrafilter.not_mem_iff, THEN iffD2])
-done
+by (rule FreeUltrafilterNat.memD)
 
 lemma FreeUltrafilterNat_Compl_mem:
-     "X\<notin> FreeUltrafilterNat ==> -X \<in> FreeUltrafilterNat"
-by (rule UltrafilterNat_mem [THEN ultrafilter.not_mem_iff, THEN iffD1])
+     "X \<notin> FreeUltrafilterNat ==> -X \<in> FreeUltrafilterNat"
+by (rule FreeUltrafilterNat.not_memD)
 
 lemma FreeUltrafilterNat_Compl_iff1:
      "(X \<notin> FreeUltrafilterNat) = (-X \<in> FreeUltrafilterNat)"
-by (rule UltrafilterNat_mem [THEN ultrafilter.not_mem_iff])
+by (rule FreeUltrafilterNat.not_mem_iff)
 
 lemma FreeUltrafilterNat_Compl_iff2:
      "(X \<in> FreeUltrafilterNat) = (-X \<notin> FreeUltrafilterNat)"
 by (auto simp add: FreeUltrafilterNat_Compl_iff1 [symmetric])
 
 lemma cofinite_mem_FreeUltrafilterNat: "finite (-X) ==> X \<in> FreeUltrafilterNat"
-apply (drule FreeUltrafilterNat_finite)  
-apply (simp add: FreeUltrafilterNat_Compl_iff2 [symmetric])
+apply (drule FreeUltrafilterNat.finite)
+apply (simp add: FreeUltrafilterNat.not_mem_iff)
 done
 
-lemma FreeUltrafilterNat_UNIV [iff]: "UNIV \<in> FreeUltrafilterNat"
-by (rule FilterNat_mem [THEN filter.UNIV])
+lemma FreeUltrafilterNat_UNIV: "UNIV \<in> FreeUltrafilterNat"
+by (rule FreeUltrafilterNat.UNIV)
 
 lemma FreeUltrafilterNat_Nat_set_refl [intro]:
      "{n. P(n) = P(n)} \<in> FreeUltrafilterNat"
@@ -202,7 +199,7 @@
 subsection{*Properties of @{term starrel}*}
 
 text{*Proving that @{term starrel} is an equivalence relation*}
-
+(*
 lemma starrel_iff: "((X,Y) \<in> starrel) = ({n. X n = Y n} \<in> FreeUltrafilterNat)"
 by (rule StarDef.starrel_iff)
 
@@ -219,21 +216,11 @@
 lemma equiv_starrel: "equiv UNIV starrel"
 by (rule StarDef.equiv_starrel)
 
-(* (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 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]
-
 lemmas eq_starrelD = eq_equiv_class [OF _ equiv_starrel]
 
-lemma lemma_starrel_refl [simp]: "x \<in> starrel `` {x}"
-by (simp add: starrel_def)
-
 lemma hypreal_empty_not_mem [simp]: "{} \<notin> star"
 apply (simp add: star_def)
 apply (auto elim!: quotientE equalityCE)
@@ -241,6 +228,16 @@
 
 lemma Rep_hypreal_nonempty [simp]: "Rep_star x \<noteq> {}"
 by (insert Rep_star [of x], auto)
+*)
+
+lemma lemma_starrel_refl [simp]: "x \<in> starrel `` {x}"
+by (simp add: starrel_def)
+
+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]
 
 subsection{*@{term hypreal_of_real}: 
             the Injection from @{typ real} to @{typ hypreal}*}