# 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