# HG changeset patch
# User wenzelm
# Date 1215105449 -7200
# Node ID c64736fe2a1f18312db3addcb02cbc52142d6783
# Parent  964766deef4731eddb33d7d311a2424a5ae23402
more precise dependencies for HOL-Word and HOL-NSA;

diff -r 964766deef47 -r c64736fe2a1f src/HOL/IsaMakefile
--- 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