# HG changeset patch
# User wenzelm
# Date 964475986 -7200
# Node ID c2dd2780f88dafaa18efbb1c1e5fa99113e11439
# Parent  8ebc549e9326d57205fdd32169b1b1fdd0d2d731
tuned;

diff -r 8ebc549e9326 -r c2dd2780f88d src/HOL/Real/ROOT.ML
--- 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";