# HG changeset patch
# User wenzelm
# Date 1185913278 -7200
# Node ID c13243a11e37e802f1d511e125e838a578d368e4
# Parent  969d334040a8d643dcc805d9f9dd3440bd25118b
removed obsolete HOL/Real/ROOT.ML;

diff -r 969d334040a8 -r c13243a11e37 src/HOL/IsaMakefile
--- 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			\
diff -r 969d334040a8 -r c13243a11e37 src/HOL/Real/ROOT.ML
--- 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";