# HG changeset patch
# User prensani
# Date 1014996283 -3600
# Node ID 7ac0a7e306db34635e390490323e858b7630f91e
# Parent  d9da3015aab4e166790483ceb68fe3405ec9443d
Completed annonce of HoareParallel

diff -r d9da3015aab4 -r 7ac0a7e306db ANNOUNCE
--- a/ANNOUNCE	Fri Mar 01 14:11:43 2002 +0100
+++ b/ANNOUNCE	Fri Mar 01 16:24:43 2002 +0100
@@ -40,8 +40,10 @@
   * HOL/Bali: large application concerning formal treatment of Java.
     (by David von Oheimb and Norbert Schirmer).
 
-  * HOL/Hoare_Parallel: large application concerning verification of
-    parallel imperative programs (Owicki-Gries method etc.)
+  * HOL/HoareParallel: large application concerning verification of
+    parallel imperative programs (Owicki-Gries method, Rely-Guarantee
+    method, verification examples: garbage collection, mutual
+    exclusion, etc.)
     (by Leonor Prensa Nieto).
 
   * HOL/GroupTheory: group theory examples including Sylow's theorem
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 \