--- a/src/HOL/Real/ROOT.ML Sat Dec 30 22:03:47 2000 +0100
+++ b/src/HOL/Real/ROOT.ML Sat Dec 30 22:13:18 2000 +0100
@@ -3,9 +3,8 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
-Construction of the Reals using Dedekind Cuts, Ultrapower Construction
-of the hyperreals, and mechanization of Nonstandard Real Analysis
- by Jacques Fleuriot
+Construction of the Reals using Dedekind Cuts
+by Jacques Fleuriot
*)
-with_path "Hyperreal" time_use_thy "Hyperreal";
+time_use_thy "Real";