--- 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)