# HG changeset patch
# User wenzelm
# Date 1273928859 -7200
# Node ID 705b58fde4764108610ef10a6378dda5f3004985
# Parent  dbd39471211c048143e2a2fe66ffe18476d578d7
more precise dependencies for HOL-Word-SMT_Examples;

diff -r dbd39471211c -r 705b58fde476 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sat May 15 13:31:25 2010 +0200
+++ b/src/HOL/IsaMakefile	Sat May 15 15:07:39 2010 +0200
@@ -60,7 +60,7 @@
   HOL-Proofs-Extraction \
   HOL-Proofs-Lambda \
   HOL-SET_Protocol \
-  HOL-SMT_Examples \
+  HOL-Word-SMT_Examples \
   HOL-Statespace \
   HOL-Subst \
       TLA-Buffer \
@@ -1254,11 +1254,11 @@
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle
 
 
-## HOL-SMT_Examples
+## HOL-Word-SMT_Examples
 
-HOL-SMT_Examples: HOL-Word $(LOG)/HOL-SMT_Examples.gz
+HOL-Word-SMT_Examples: HOL-Word $(LOG)/HOL-Word-SMT_Examples.gz
 
-$(LOG)/HOL-SMT_Examples.gz: $(OUT)/HOL-Word SMT_Examples/ROOT.ML	\
+$(LOG)/HOL-Word-SMT_Examples.gz: $(OUT)/HOL-Word SMT_Examples/ROOT.ML	\
   SMT_Examples/SMT_Examples.thy SMT_Examples/SMT_Examples.certs		\
   SMT_Examples/SMT_Word_Examples.thy SMT_Examples/SMT_Tests.thy		\
   SMT_Examples/SMT_Word_Examples.certs SMT_Examples/SMT_Tests.certs
@@ -1346,15 +1346,15 @@
 		$(LOG)/HOL-Probability.gz $(LOG)/HOL-Prolog.gz		\
 		$(LOG)/HOL-Proofs.gz $(LOG)/HOL-Proofs-Extraction.gz	\
 		$(LOG)/HOL-Proofs-Lambda.gz $(LOG)/HOL-SET_Protocol.gz	\
-		$(LOG)/HOL-SMT_Examples.gz $(LOG)/HOL-Statespace.gz 	\
-		$(LOG)/HOL-Subst.gz $(LOG)/HOL-UNITY.gz			\
-		$(LOG)/HOL-Unix.gz $(LOG)/HOL-Word-Examples.gz		\
-		$(LOG)/HOL-Word.gz $(LOG)/HOL-ZF.gz $(LOG)/HOL-ex.gz	\
-		$(LOG)/HOL.gz $(LOG)/HOL4.gz $(LOG)/TLA-Buffer.gz	\
-		$(LOG)/TLA-Inc.gz $(LOG)/TLA-Memory.gz $(LOG)/TLA.gz	\
-		$(OUT)/HOL $(OUT)/HOL-Algebra $(OUT)/HOL-Base		\
-		$(OUT)/HOL-Boogie $(OUT)/HOL-Main			\
-		$(OUT)/HOL-Multivariate_Analysis $(OUT)/HOL-NSA		\
-		$(OUT)/HOL-Nominal $(OUT)/HOL-Plain			\
+		$(LOG)/HOL-Word-SMT_Examples.gz				\
+		$(LOG)/HOL-Statespace.gz $(LOG)/HOL-Subst.gz		\
+		$(LOG)/HOL-UNITY.gz $(LOG)/HOL-Unix.gz			\
+		$(LOG)/HOL-Word-Examples.gz $(LOG)/HOL-Word.gz		\
+		$(LOG)/HOL-ZF.gz $(LOG)/HOL-ex.gz $(LOG)/HOL.gz		\
+		$(LOG)/HOL4.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Inc.gz	\
+		$(LOG)/TLA-Memory.gz $(LOG)/TLA.gz $(OUT)/HOL		\
+		$(OUT)/HOL-Algebra $(OUT)/HOL-Base $(OUT)/HOL-Boogie	\
+		$(OUT)/HOL-Main $(OUT)/HOL-Multivariate_Analysis	\
+		$(OUT)/HOL-NSA $(OUT)/HOL-Nominal $(OUT)/HOL-Plain	\
 		$(OUT)/HOL-Probability $(OUT)/HOL-Proofs		\
 		$(OUT)/HOL-Word $(OUT)/HOL4 $(OUT)/TLA