src/HOL/IsaMakefile
changeset 16782 b214f21ae396
parent 16733 236dfafbeb63
child 16784 92ff7c903585
--- a/src/HOL/IsaMakefile	Tue Jul 12 19:29:52 2005 +0200
+++ b/src/HOL/IsaMakefile	Tue Jul 12 21:49:38 2005 +0200
@@ -143,6 +143,7 @@
   Real/Rational.thy Real/PReal.thy Real/RComplete.thy				\
   Real/ROOT.ML Real/Real.thy Real/real_arith.ML Real/RealDef.thy		\
   Real/RealPow.thy Real/document/root.tex					\
+  Real/Float.thy Real/Float.ML                                                  \
   Hyperreal/EvenOdd.thy Hyperreal/Fact.thy Hyperreal/HLog.thy			\
   Hyperreal/Filter.thy Hyperreal/HSeries.thy					\
   Hyperreal/HTranscendental.thy Hyperreal/HyperArith.thy			\