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 \