--- a/src/HOL/IsaMakefile Thu Nov 15 15:07:16 2001 +0100
+++ b/src/HOL/IsaMakefile Thu Nov 15 16:12:49 2001 +0100
@@ -131,20 +131,23 @@
HOL-Real-Hyperreal: HOL-Real $(LOG)/HOL-Real-Hyperreal.gz
-$(LOG)/HOL-Real-Hyperreal.gz: $(OUT)/HOL-Real \
- Hyperreal/Filter.ML Hyperreal/Filter.thy Hyperreal/HRealAbs.ML \
- Hyperreal/HRealAbs.thy Hyperreal/HSeries.ML Hyperreal/HSeries.thy \
- Hyperreal/HyperArith.thy Hyperreal/HyperArith0.ML \
- Hyperreal/HyperArith0.thy 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/NSA.ML Hyperreal/NSA.thy Hyperreal/NatStar.ML \
- Hyperreal/NatStar.thy Hyperreal/ROOT.ML Hyperreal/SEQ.ML \
- Hyperreal/SEQ.thy Hyperreal/Series.ML Hyperreal/Series.thy \
- Hyperreal/Star.ML Hyperreal/Star.thy Hyperreal/Zorn.ML \
- Hyperreal/Zorn.thy Hyperreal/fuf.ML Hyperreal/hypreal_arith.ML \
+$(LOG)/HOL-Real-Hyperreal.gz: $(OUT)/HOL-Real Hyperreal/ROOT.ML\
+ Hyperreal/EvenOdd.ML Hyperreal/EvenOdd.thy Hyperreal/ExtraThms2.ML\
+ Hyperreal/ExtraThms2.thy Hyperreal/Fact.ML Hyperreal/Fact.thy\
+ Hyperreal/Filter.ML Hyperreal/Filter.thy Hyperreal/HRealAbs.ML\
+ Hyperreal/HRealAbs.thy Hyperreal/HSeries.ML Hyperreal/HSeries.thy\
+ Hyperreal/HyperArith0.ML Hyperreal/HyperArith0.thy Hyperreal/HyperArith.thy\
+ 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/NSA.ML Hyperreal/NSA.thy\
+ Hyperreal/NthRoot.ML Hyperreal/NthRoot.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\
+ Hyperreal/fuf.ML Hyperreal/hypreal_arith.ML \
Hyperreal/hypreal_arith0.ML
@$(ISATOOL) usedir $(OUT)/HOL-Real Hyperreal