--- a/src/HOL/Real/ROOT.ML Thu Sep 21 10:42:49 2000 +0200
+++ b/src/HOL/Real/ROOT.ML Thu Sep 21 12:11:38 2000 +0200
@@ -3,7 +3,13 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
-Construction of the Reals using Dedekind Cuts, by Jacques Fleuriot
+Construction of the Reals using Dedekind Cuts, Ultrapower Construction
+of the hyperreals, and mechanization of Nonstandard Real Analysis
+ by Jacques Fleuriot
*)
-with_path "Hyperreal" use_thy "HyperDef";
+time_use_thy "Real";
+with_path "Hyperreal" use_thy "Series";
+
+
+