--- a/src/HOL/IsaMakefile Sun Aug 21 22:13:04 2011 +0200
+++ b/src/HOL/IsaMakefile Sun Aug 21 22:13:04 2011 +0200
@@ -70,7 +70,6 @@
HOL-SPARK-Examples \
HOL-Word-SMT_Examples \
HOL-Statespace \
- HOL-Subst \
TLA-Buffer \
TLA-Inc \
TLA-Memory \
@@ -496,15 +495,6 @@
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hahn_Banach
-## HOL-Subst
-
-HOL-Subst: HOL $(LOG)/HOL-Subst.gz
-
-$(LOG)/HOL-Subst.gz: $(OUT)/HOL Subst/AList.thy Subst/ROOT.ML \
- Subst/Subst.thy Subst/UTerm.thy Subst/Unifier.thy Subst/Unify.thy
- @$(ISABELLE_TOOL) usedir $(OUT)/HOL Subst
-
-
## HOL-Induct
HOL-Induct: HOL $(LOG)/HOL-Induct.gz
@@ -1754,7 +1744,7 @@
$(LOG)/HOL-Proofs-Lambda.gz $(LOG)/HOL-SET_Protocol.gz \
$(LOG)/HOL-Word-SMT_Examples.gz \
$(LOG)/HOL-SPARK.gz $(LOG)/HOL-SPARK-Examples.gz \
- $(LOG)/HOL-Statespace.gz $(LOG)/HOL-Subst.gz \
+ $(LOG)/HOL-Statespace.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 \