--- a/src/HOL/IsaMakefile Thu Jul 03 19:02:33 2008 +0200
+++ b/src/HOL/IsaMakefile Thu Jul 03 19:17:29 2008 +0200
@@ -516,6 +516,7 @@
Algebra/poly/UnivPoly2.thy Algebra/ringsimp.ML
@cd Algebra; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Algebra
+
## HOL-Auth
HOL-Auth: HOL $(LOG)/HOL-Auth.gz
@@ -574,6 +575,7 @@
Unix/document/root.bib Unix/document/root.tex
@$(ISATOOL) usedir $(OUT)/HOL Unix
+
## HOL-ZF
HOL-ZF: HOL $(LOG)/HOL-ZF.gz
@@ -582,6 +584,7 @@
ZF/HOLZF.thy ZF/MainZF.thy ZF/Games.thy ZF/document/root.tex
@$(ISATOOL) usedir $(OUT)/HOL ZF
+
## HOL-Modelcheck
HOL-Modelcheck: HOL $(LOG)/HOL-Modelcheck.gz
@@ -593,6 +596,7 @@
Modelcheck/ROOT.ML Modelcheck/mucke_oracle.ML
@$(ISATOOL) usedir $(OUT)/HOL Modelcheck
+
## HOL-SizeChange
HOL-SizeChange: HOL $(LOG)/HOL-SizeChange.gz
@@ -605,6 +609,7 @@
SizeChange/sct.ML SizeChange/ROOT.ML
@$(ISATOOL) usedir $(OUT)/HOL SizeChange
+
## HOL-Lambda
HOL-Lambda: HOL $(LOG)/HOL-Lambda.gz
@@ -931,6 +936,7 @@
Word/Examples/WordExamples.thy
@cd Word; $(ISATOOL) usedir $(OUT)/HOL-Word Examples
+
## HOL-Statespace
HOL-Statespace: HOL $(LOG)/HOL-Statespace.gz
@@ -942,11 +948,12 @@
Statespace/state_fun.ML Statespace/document/root.tex
@$(ISATOOL) usedir -g true $(OUT)/HOL Statespace
+
## HOL-NSA
-HOL-NSA: HOL $(LOG)/HOL-NSA.gz
+HOL-NSA: HOL $(OUT)/HOL-NSA
-$(LOG)/HOL-NSA.gz: $(OUT)/HOL \
+$(OUT)/HOL-NSA: $(OUT)/HOL \
NSA/CLim.thy \
NSA/CStar.thy \
NSA/NSCA.thy \
@@ -973,6 +980,7 @@
NSA/ROOT.ML
@cd NSA; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-NSA
+
## HOL-NSA-Examples
HOL-NSA-Examples: HOL-NSA $(LOG)/HOL-NSA-Examples.gz
@@ -981,6 +989,7 @@
NSA/Examples/NSPrimes.thy
@cd NSA; $(ISATOOL) usedir $(OUT)/HOL-NSA Examples
+
## clean
clean:
@@ -1000,4 +1009,6 @@
$(LOG)/HOL-Lattice $(LOG)/HOL-Matrix \
$(LOG)/HOL-HahnBanach.gz $(LOG)/HOL-SET-Protocol.gz \
$(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz \
- $(LOG)/HOL-Library.gz $(LOG)/HOL-Unix.gz
+ $(LOG)/HOL-Library.gz $(LOG)/HOL-Unix.gz \
+ $(OUT)/HOL-Word $(LOG)/HOL-Word.gz $(LOG)/HOL-Word-Examples.gz \
+ $(OUT)/HOL-NSA $(LOG)/HOL-NSA.gz $(LOG)/HOL-NSA-Examples.gz