src/HOL/IsaMakefile
changeset 15094 a7d1a3fdc30d
parent 15093 49ede01e9ee6
child 15103 79846e8792eb
--- a/src/HOL/IsaMakefile	Fri Jul 30 18:37:58 2004 +0200
+++ b/src/HOL/IsaMakefile	Sat Jul 31 20:54:23 2004 +0200
@@ -144,10 +144,9 @@
   Real/Lubs.thy Real/rat_arith.ML\
   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/real_arith.ML\
-  Hyperreal/EvenOdd.thy\
-  Hyperreal/Fact.ML Hyperreal/Fact.thy Hyperreal/HLog.thy\
-  Hyperreal/Filter.ML Hyperreal/Filter.thy Hyperreal/HSeries.thy\
+  Real/RealPow.thy Real/document/root.tex\
+  Hyperreal/EvenOdd.thy Hyperreal/Fact.thy Hyperreal/HLog.thy\
+  Hyperreal/Filter.thy Hyperreal/HSeries.thy\
   Hyperreal/HTranscendental.thy Hyperreal/HyperArith.thy\
   Hyperreal/HyperDef.thy Hyperreal/HyperNat.thy\
   Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\