# HG changeset patch
# User oheimb
# Date 949425489 -3600
# Node ID 6a0b1037bab3e944da79f9eb15bee7d708288783
# Parent  a6a4fb7b819b66cf5f12cde10780c662d4ebfe47
added forgotten rules to make IMPP

diff -r a6a4fb7b819b -r 6a0b1037bab3 src/HOL/IsaMakefile
--- 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		\