src/HOL/IsaMakefile
changeset 14269 502a7c95de73
parent 14268 5cf13e80be0e
child 14272 5efbb548107d
--- a/src/HOL/IsaMakefile	Thu Nov 27 10:47:55 2003 +0100
+++ b/src/HOL/IsaMakefile	Fri Nov 28 12:09:37 2003 +0100
@@ -141,10 +141,10 @@
   Real/Lubs.ML 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/ROOT.ML Real/Real.thy \
   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/RealBin.thy Real/RealDef.thy \
   Real/RealInt.thy Real/RealOrd.thy \
   Real/RealPow.thy Real/document/root.tex Real/real_arith.ML\
   Hyperreal/EvenOdd.ML Hyperreal/EvenOdd.thy \