tuned;

--- a/src/HOL/Real/ROOT.ML	Mon Jul 24 23:59:32 2000 +0200
+++ b/src/HOL/Real/ROOT.ML	Mon Jul 24 23:59:46 2000 +0200
@@ -4,8 +4,6 @@
     Copyright   1998  University of Cambridge
 
 Construction of the Reals using Dedekind Cuts, by Jacques Fleuriot
-
-Linear real arithmetic is installed in RealBin.ML.
 *)
 
 with_path "Hyperreal" use_thy "HyperDef";