src/HOL/IsaMakefile
changeset 12196 a3be6b3a9c0b
parent 12101 a79681a01f41
child 12224 02df7cbe7d25
--- 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