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