--- a/src/HOL/IsaMakefile Tue Feb 01 12:26:47 2000 +0100
+++ b/src/HOL/IsaMakefile Tue Feb 01 18:18:09 2000 +0100
@@ -151,6 +151,16 @@
@$(ISATOOL) usedir $(OUT)/HOL IMP
+## HOL-IMPP
+
+HOL-IMPP: HOL $(LOG)/HOL-IMPP.gz
+
+$(LOG)/HOL-IMPP.gz: $(OUT)/HOL IMPP/ROOT.ML IMPP/Com.thy IMPP/Com.ML \
+ IMPP/Natural.thy IMPP/Natural.ML IMPP/Hoare.thy IMPP/Hoare.ML \
+ IMPP/Misc.thy IMPP/Misc.ML IMPP/EvenOdd.thy IMPP/EvenOdd.ML
+ @$(ISATOOL) usedir $(OUT)/HOL IMPP
+
+
## HOL-Hoare
HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz
@@ -478,8 +488,9 @@
clean:
@rm -f $(OUT)/HOL $(OUT)/HOL-Real $(LOG)/HOL.gz $(LOG)/HOL-Subst.gz \
- $(LOG)/HOL-Induct.gz $(LOG)/HOL-IMP.gz $(LOG)/HOL-Hoare.gz \
- $(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
+ $(LOG)/HOL-IMP.gz $(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz \
+ $(LOG)/HOL-Induct.gz $(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz \
+ $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
$(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
$(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz $(LOG)/HOL-BCV.gz $(LOG)/HOL-IOA.gz \
$(LOG)/HOL-AxClasses-Group.gz \