1.1 --- a/src/HOL/IsaMakefile	Tue Jul 31 21:19:24 2007 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Jul 31 22:21:18 2007 +0200
     1.3 @@ -160,7 +160,7 @@
     1.4  $(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML $(SRC)/Tools/float.ML \
     1.5    Library/Zorn.thy							\
     1.6    Real/ContNotDenum.thy Real/float_arith.ML Real/Float.thy		\
     1.7 -  Real/Lubs.thy Real/PReal.thy Real/RComplete.thy Real/ROOT.ML		\
     1.8 +  Real/Lubs.thy Real/PReal.thy Real/RComplete.thy 			\
     1.9    Real/Rational.thy Real/Real.thy Real/RealDef.thy Real/RealPow.thy	\
    1.10    Real/RealVector.thy Real/rat_arith.ML Real/real_arith.ML		\
    1.11    Hyperreal/StarDef.thy Hyperreal/StarClasses.thy			\

     2.1 --- a/src/HOL/Real/ROOT.ML	Tue Jul 31 21:19:24 2007 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,10 +0,0 @@
     2.4 -(*  Title:      HOL/Real/ROOT.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 -    Copyright   1998  University of Cambridge
     2.8 -
     2.9 -Construction of the Reals using Dedekind Cuts 
    2.10 -by Jacques Fleuriot
    2.11 -*)
    2.12 -
    2.13 -time_use_thy "Float";