# HG changeset patch
# User nipkow
# Date 977422758 -3600
# Node ID 819ee80305a8fa6ede6839bfcdef192cd09b5a5f
# Parent  439e44031b815c5a6dc336e413f95ca2e1606320
*** empty log message ***

diff -r 439e44031b81 -r 819ee80305a8 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Dec 21 18:57:39 2000 +0100
+++ b/src/HOL/IsaMakefile	Thu Dec 21 19:19:18 2000 +0100
@@ -125,7 +125,8 @@
   Real/Lubs.thy Real/PNat.ML Real/PNat.thy Real/PRat.ML Real/PRat.thy \
   Real/PReal.ML Real/PReal.thy Real/RComplete.ML Real/RComplete.thy \
   Real/ROOT.ML Real/Real.thy Real/RealAbs.ML Real/RealAbs.thy \
-  Real/RealArith.ML Real/RealArith.thy Real/RealBin.ML \
+  Real/RealArith0.ML Real/RealArith0.thy Real/real_arith0.ML \
+  Real/RealArith.thy Real/real_arith.ML Real/RealBin.ML \
   Real/RealBin.thy Real/RealDef.ML Real/RealDef.thy Real/RealInt.ML \
   Real/RealInt.thy Real/RealOrd.ML Real/RealOrd.thy Real/RealPow.ML \
   Real/RealPow.thy Real/real_arith.ML