diff -r 5ddbdbadba06 -r 0848ab6fe5fc src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Thu Apr 22 11:02:22 2004 +0200
+++ b/src/HOL/Hyperreal/NSA.thy	Thu Apr 22 12:11:17 2004 +0200
@@ -20,6 +20,10 @@
   HInfinite :: "hypreal set"
    "HInfinite == {x. \<forall>r \<in> Reals. r < abs x}"
 
+  (* infinitely close *)
+  approx :: "[hypreal, hypreal] => bool"    (infixl "@=" 50)
+   "x @= y       == (x + -y) \<in> Infinitesimal"
+
   (* standard part map *)
   st        :: "hypreal => hypreal"
    "st           == (%x. @r. x \<in> HFinite & r \<in> Reals & r @= x)"
@@ -30,10 +34,6 @@
   galaxy    :: "hypreal => hypreal set"
    "galaxy x     == {y. (x + -y) \<in> HFinite}"
 
-  (* infinitely close *)
-  approx :: "[hypreal, hypreal] => bool"    (infixl "@=" 50)
-   "x @= y       == (x + -y) \<in> Infinitesimal"
-
 
 defs (overloaded)