diff -r d9da3015aab4 -r 7ac0a7e306db src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Mar 01 14:11:43 2002 +0100
+++ b/src/HOL/IsaMakefile	Fri Mar 01 16:24:43 2002 +0100
@@ -21,6 +21,7 @@
       HOL-Real-HahnBanach \
       HOL-Real-ex \
   HOL-Hoare \
+  HOL-HoareParallel \
   HOL-IMP \
   HOL-IMPP \
   HOL-IOA \
@@ -286,6 +287,22 @@
 	@$(ISATOOL) usedir $(OUT)/HOL Hoare
 
 
+## HOL-HoareParallel
+
+HOL-HoareParallel: HOL $(LOG)/HOL-HoareParallel.gz
+
+$(LOG)/HOL-HoareParallel.gz: $(OUT)/HOL HoareParallel/Gar_Coll.thy \
+  HoareParallel/Graph.thy HoareParallel/Mul_Gar_Coll.thy	   \
+  HoareParallel/OG_Com.thy HoareParallel/OG_Examples.thy	   \
+  HoareParallel/OG_Hoare.thy HoareParallel/OG_Syntax.thy	   \
+  HoareParallel/OG_Tactics.thy HoareParallel/OG_Tran.thy	   \
+  HoareParallel/RG_Com.thy HoareParallel/RG_Examples.thy	   \
+  HoareParallel/RG_Hoare.thy HoareParallel/RG_Syntax.thy	   \
+  HoareParallel/RG_Tran.thy HoareParallel/ROOT.ML		   \
+  HoareParallel/document/root.tex
+	@$(ISATOOL) usedir $(OUT)/HOL HoareParallel
+
+
 ## HOL-Lex
 
 HOL-Lex: HOL $(LOG)/HOL-Lex.gz
@@ -625,6 +642,7 @@
 		$(LOG)/HOL-Isar_examples.gz $(LOG)/HOL-Induct.gz \
 		$(LOG)/HOL-ex.gz $(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz \
 		$(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz \
+		$(LOG)/HOL-HoareParallel.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 \