--- a/src/HOL/IsaMakefile Tue Jul 31 21:19:24 2007 +0200
+++ b/src/HOL/IsaMakefile Tue Jul 31 22:21:18 2007 +0200
@@ -160,7 +160,7 @@
$(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML $(SRC)/Tools/float.ML \
Library/Zorn.thy \
Real/ContNotDenum.thy Real/float_arith.ML Real/Float.thy \
- Real/Lubs.thy Real/PReal.thy Real/RComplete.thy Real/ROOT.ML \
+ Real/Lubs.thy Real/PReal.thy Real/RComplete.thy \
Real/Rational.thy Real/Real.thy Real/RealDef.thy Real/RealPow.thy \
Real/RealVector.thy Real/rat_arith.ML Real/real_arith.ML \
Hyperreal/StarDef.thy Hyperreal/StarClasses.thy \
--- a/src/HOL/Real/ROOT.ML Tue Jul 31 21:19:24 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-(* Title: HOL/Real/ROOT.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1998 University of Cambridge
-
-Construction of the Reals using Dedekind Cuts
-by Jacques Fleuriot
-*)
-
-time_use_thy "Float";