Completed annonce of HoareParallel
authorprensani
Fri Mar 01 16:24:43 2002 +0100 (2002-03-01)
changeset 129967ac0a7e306db
parent 12995 d9da3015aab4
child 12997 80dec7322a8c
Completed annonce of HoareParallel
ANNOUNCE
src/HOL/IsaMakefile
     1.1 --- a/ANNOUNCE	Fri Mar 01 14:11:43 2002 +0100
     1.2 +++ b/ANNOUNCE	Fri Mar 01 16:24:43 2002 +0100
     1.3 @@ -40,8 +40,10 @@
     1.4    * HOL/Bali: large application concerning formal treatment of Java.
     1.5      (by David von Oheimb and Norbert Schirmer).
     1.6  
     1.7 -  * HOL/Hoare_Parallel: large application concerning verification of
     1.8 -    parallel imperative programs (Owicki-Gries method etc.)
     1.9 +  * HOL/HoareParallel: large application concerning verification of
    1.10 +    parallel imperative programs (Owicki-Gries method, Rely-Guarantee
    1.11 +    method, verification examples: garbage collection, mutual
    1.12 +    exclusion, etc.)
    1.13      (by Leonor Prensa Nieto).
    1.14  
    1.15    * HOL/GroupTheory: group theory examples including Sylow's theorem
     2.1 --- a/src/HOL/IsaMakefile	Fri Mar 01 14:11:43 2002 +0100
     2.2 +++ b/src/HOL/IsaMakefile	Fri Mar 01 16:24:43 2002 +0100
     2.3 @@ -21,6 +21,7 @@
     2.4        HOL-Real-HahnBanach \
     2.5        HOL-Real-ex \
     2.6    HOL-Hoare \
     2.7 +  HOL-HoareParallel \
     2.8    HOL-IMP \
     2.9    HOL-IMPP \
    2.10    HOL-IOA \
    2.11 @@ -286,6 +287,22 @@
    2.12  	@$(ISATOOL) usedir $(OUT)/HOL Hoare
    2.13  
    2.14  
    2.15 +## HOL-HoareParallel
    2.16 +
    2.17 +HOL-HoareParallel: HOL $(LOG)/HOL-HoareParallel.gz
    2.18 +
    2.19 +$(LOG)/HOL-HoareParallel.gz: $(OUT)/HOL HoareParallel/Gar_Coll.thy \
    2.20 +  HoareParallel/Graph.thy HoareParallel/Mul_Gar_Coll.thy	   \
    2.21 +  HoareParallel/OG_Com.thy HoareParallel/OG_Examples.thy	   \
    2.22 +  HoareParallel/OG_Hoare.thy HoareParallel/OG_Syntax.thy	   \
    2.23 +  HoareParallel/OG_Tactics.thy HoareParallel/OG_Tran.thy	   \
    2.24 +  HoareParallel/RG_Com.thy HoareParallel/RG_Examples.thy	   \
    2.25 +  HoareParallel/RG_Hoare.thy HoareParallel/RG_Syntax.thy	   \
    2.26 +  HoareParallel/RG_Tran.thy HoareParallel/ROOT.ML		   \
    2.27 +  HoareParallel/document/root.tex
    2.28 +	@$(ISATOOL) usedir $(OUT)/HOL HoareParallel
    2.29 +
    2.30 +
    2.31  ## HOL-Lex
    2.32  
    2.33  HOL-Lex: HOL $(LOG)/HOL-Lex.gz
    2.34 @@ -625,6 +642,7 @@
    2.35  		$(LOG)/HOL-Isar_examples.gz $(LOG)/HOL-Induct.gz \
    2.36  		$(LOG)/HOL-ex.gz $(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz \
    2.37  		$(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz \
    2.38 +		$(LOG)/HOL-HoareParallel.gz \
    2.39  		$(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz \
    2.40  		$(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
    2.41  		$(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \