1.1 --- a/src/HOL/IsaMakefile Tue Jan 08 20:52:46 2002 +0100
1.2 +++ b/src/HOL/IsaMakefile Tue Jan 08 21:02:15 2002 +0100
1.3 @@ -7,7 +7,7 @@
1.4 ## targets
1.5
1.6 default: HOL
1.7 -images: HOL HOL-Real TLA
1.8 +images: HOL HOL-Real HOL-Hyperreal TLA
1.9
1.10 #Note: keep targets sorted (except for HOL-Library)
1.11 test: \
1.12 @@ -128,9 +128,9 @@
1.13
1.14 ## HOL-Real-Hyperreal
1.15
1.16 -HOL-Real-Hyperreal: HOL-Real $(LOG)/HOL-Real-Hyperreal.gz
1.17 +HOL-Hyperreal: HOL-Real $(OUT)/HOL-Hyperreal
1.18
1.19 -$(LOG)/HOL-Real-Hyperreal.gz: $(OUT)/HOL-Real Hyperreal/ROOT.ML\
1.20 +$(OUT)/HOL-Hyperreal: $(OUT)/HOL-Real Hyperreal/ROOT.ML\
1.21 Hyperreal/EvenOdd.ML Hyperreal/EvenOdd.thy Hyperreal/ExtraThms2.ML\
1.22 Hyperreal/ExtraThms2.thy Hyperreal/Fact.ML Hyperreal/Fact.thy\
1.23 Hyperreal/Filter.ML Hyperreal/Filter.thy Hyperreal/HRealAbs.ML\
1.24 @@ -151,7 +151,7 @@
1.25 Hyperreal/Transcendental.thy Hyperreal/Zorn.ML Hyperreal/Zorn.thy\
1.26 Hyperreal/fuf.ML Hyperreal/hypreal_arith.ML \
1.27 Hyperreal/hypreal_arith0.ML
1.28 - @$(ISATOOL) usedir $(OUT)/HOL-Real Hyperreal
1.29 + @cd Hyperreal; $(ISATOOL) usedir -b $(OUT)/HOL-Real HOL-Hyperreal
1.30
1.31
1.32 ## HOL-Real-ex
1.33 @@ -610,7 +610,7 @@
1.34 ## clean
1.35
1.36 clean:
1.37 - @rm -f $(OUT)/HOL $(OUT)/HOL-Real $(OUT)/TLA \
1.38 + @rm -f $(OUT)/HOL $(OUT)/HOL-Real $(OUT)/HOL-Hyperreal $(OUT)/TLA \
1.39 $(LOG)/HOL.gz $(LOG)/HOL-Real.gz $(LOG)/TLA.gz \
1.40 $(LOG)/HOL-Isar_examples.gz $(LOG)/HOL-Induct.gz \
1.41 $(LOG)/HOL-ex.gz $(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz \
1.42 @@ -622,7 +622,6 @@
1.43 $(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz \
1.44 $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
1.45 $(LOG)/HOL-Lattice $(LOG)/HOL-Real-ex.gz \
1.46 - $(LOG)/HOL-Real-Hyperreal.gz \
1.47 $(LOG)/HOL-Real-HahnBanach.gz $(LOG)/TLA-Inc.gz \
1.48 $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz \
1.49 $(LOG)/HOL-Library.gz $(LOG)/HOL-Unix.gz