diff -r b0064703967b -r c78c7da09519 src/HOL/Hyperreal/NSA.thy
--- 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