src/HOL/IsaMakefile

 
 ## HOL-Complex
 
 HOL-Complex: HOL $(OUT)/HOL-Complex
 
-$(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML $(SRC)/Tools/float.ML	\
+$(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML                          \
   Library/Zorn.thy Library/Order_Relation.thy Real/ContNotDenum.thy	\
-  Real/float_arith.ML Real/Float.thy Real/Lubs.thy Real/PReal.thy	\
+  Real/float_arith.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/Fact.thy		\
   Hyperreal/HLog.thy Hyperreal/Filter.thy Hyperreal/HSeries.thy		\
   Hyperreal/transfer.ML Hyperreal/HLim.thy Hyperreal/HSEQ.thy		\

   Library/Code_Message.thy Library/Abstract_Rat.thy			\
   Library/Univ_Poly.thy Library/Numeral_Type.thy			\
   Library/Boolean_Algebra.thy Library/Countable.thy Library/RType.thy	\
   Library/Heap.thy Library/Heap_Monad.thy Library/Array.thy		\
   Library/Ref.thy Library/Imperative_HOL.thy Library/RBT.thy		\
-  Library/Enum.thy
+  Library/Enum.thy Real/Float.thy $(SRC)/Tools/float.ML
 	@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library
 
 
 ## HOL-Subst