src/HOL/IsaMakefile
changeset 12224 02df7cbe7d25
parent 12196 a3be6b3a9c0b
child 12246 fdb65a05fca8
--- a/src/HOL/IsaMakefile	Fri Nov 16 15:25:17 2001 +0100
+++ b/src/HOL/IsaMakefile	Fri Nov 16 18:24:11 2001 +0100
@@ -140,10 +140,13 @@
   Hyperreal/HyperBin.ML Hyperreal/HyperBin.thy Hyperreal/HyperDef.ML\
   Hyperreal/HyperDef.thy Hyperreal/HyperNat.ML Hyperreal/HyperNat.thy\
   Hyperreal/HyperOrd.ML Hyperreal/HyperOrd.thy Hyperreal/HyperPow.ML\
-  Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy Hyperreal/Lim.ML\
-  Hyperreal/Lim.thy Hyperreal/NatStar.ML Hyperreal/NatStar.thy\
+  Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\
+  Hyperreal/Lim.ML Hyperreal/Lim.thy  Hyperreal/Log.ML Hyperreal/Log.thy\
+  Hyperreal/MacLaurin.ML Hyperreal/MacLaurin.thy\
+  Hyperreal/NatStar.ML Hyperreal/NatStar.thy\
   Hyperreal/NSA.ML Hyperreal/NSA.thy\
   Hyperreal/NthRoot.ML Hyperreal/NthRoot.thy\
+  Hyperreal/Poly.ML Hyperreal/Poly.thy\
   Hyperreal/SEQ.ML Hyperreal/SEQ.thy Hyperreal/Series.ML Hyperreal/Series.thy\
   Hyperreal/Star.ML Hyperreal/Star.thy Hyperreal/Transcendental.ML\
   Hyperreal/Transcendental.thy Hyperreal/Zorn.ML Hyperreal/Zorn.thy\