--- 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
--- 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 \