--- 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