src/HOL/IsaMakefile
changeset 24103 c13243a11e37
parent 24091 109f19a13872
child 24127 a56b6ed2e49c
--- 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			\