--- a/src/HOL/Hyperreal/NSA.thy Thu Jan 29 16:51:17 2004 +0100
+++ b/src/HOL/Hyperreal/NSA.thy Mon Feb 02 12:23:46 2004 +0100
@@ -5,7 +5,7 @@
header{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*}
-theory NSA = HRealAbs + RComplete:
+theory NSA = HyperArith + RComplete:
constdefs