--- 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\