| changeset 7583 | d1b40e0464b1 |
| parent 7334 | a90fc1e5fb19 |
| child 7933 | 80b528790ccc |
--- a/src/HOL/Real/ROOT.ML Thu Sep 23 09:04:36 1999 +0200 +++ b/src/HOL/Real/ROOT.ML Thu Sep 23 09:05:44 1999 +0200 @@ -4,6 +4,8 @@ Copyright 1998 University of Cambridge Construction of the Reals using Dedekind Cuts, by Jacques Fleuriot + +Linear real arithmetic is installed in RealBin.ML. *) writeln"Root file for HOL/Real";