Mercurialisabelle / diff
summary | shortlog | changelog | graph | tags | branches | files | changeset | file | revisions | annotate | diff | raw
src/HOL/IsaMakefile
changeset 32621 a073cb249a06
parent 32618 42865636d006
child 32624 3dec57ec3473 
     1.1 --- a/src/HOL/IsaMakefile	Mon Sep 21 08:45:31 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Sep 21 10:58:25 2009 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4    HOL-Extraction \
     1.5    HOL-Hahn_Banach \
     1.6    HOL-Hoare \
     1.7 -  HOL-HoareParallel \
     1.8 +  HOL-Hoare_Parallel \
     1.9    HOL-Import \
    1.10    HOL-IMP \
    1.11    HOL-IMPP \
    1.12 @@ -537,21 +537,22 @@
    1.13  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Hoare
    1.14  
    1.15  
    1.16 -## HOL-HoareParallel
    1.17 +## HOL-Hoare_Parallel
    1.18  
    1.19 -HOL-HoareParallel: HOL $(LOG)/HOL-HoareParallel.gz
    1.20 +HOL-Hoare_Parallel: HOL $(LOG)/HOL-Hoare_Parallel.gz
    1.21  
    1.22 -$(LOG)/HOL-HoareParallel.gz: $(OUT)/HOL HoareParallel/Gar_Coll.thy	\
    1.23 -  HoareParallel/Graph.thy HoareParallel/Mul_Gar_Coll.thy		\
    1.24 -  HoareParallel/OG_Com.thy HoareParallel/OG_Examples.thy		\
    1.25 -  HoareParallel/OG_Hoare.thy HoareParallel/OG_Syntax.thy		\
    1.26 -  HoareParallel/OG_Tactics.thy HoareParallel/OG_Tran.thy		\
    1.27 -  HoareParallel/Quote_Antiquote.thy HoareParallel/RG_Com.thy		\
    1.28 -  HoareParallel/RG_Examples.thy HoareParallel/RG_Hoare.thy		\
    1.29 -  HoareParallel/RG_Syntax.thy HoareParallel/RG_Tran.thy			\
    1.30 -  HoareParallel/ROOT.ML HoareParallel/document/root.tex			\
    1.31 -  HoareParallel/document/root.bib
    1.32 -	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL HoareParallel
    1.33 +$(LOG)/HOL-Hoare_Parallel.gz: $(OUT)/HOL Hoare_Parallel/Gar_Coll.thy	\
    1.34 +  Hoare_Parallel/Graph.thy Hoare_Parallel/Hoare_Parallel.thy	\
    1.35 +  Hoare_Parallel/Mul_Gar_Coll.thy		\
    1.36 +  Hoare_Parallel/OG_Com.thy Hoare_Parallel/OG_Examples.thy		\
    1.37 +  Hoare_Parallel/OG_Hoare.thy Hoare_Parallel/OG_Syntax.thy		\
    1.38 +  Hoare_Parallel/OG_Tactics.thy Hoare_Parallel/OG_Tran.thy		\
    1.39 +  Hoare_Parallel/Quote_Antiquote.thy Hoare_Parallel/RG_Com.thy		\
    1.40 +  Hoare_Parallel/RG_Examples.thy Hoare_Parallel/RG_Hoare.thy		\
    1.41 +  Hoare_Parallel/RG_Syntax.thy Hoare_Parallel/RG_Tran.thy			\
    1.42 +  Hoare_Parallel/ROOT.ML Hoare_Parallel/document/root.tex			\
    1.43 +  Hoare_Parallel/document/root.bib
    1.44 +	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hoare_Parallel
    1.45  
    1.46  
    1.47  ## HOL-MetisExamples
    1.48 @@ -1157,7 +1158,7 @@
    1.49  		$(LOG)/HOL-Induct.gz $(LOG)/HOL-ex.gz			\
    1.50  		$(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz			\
    1.51  		$(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz			\
    1.52 -		$(LOG)/HOL-HoareParallel.gz $(LOG)/HOL-Lex.gz		\
    1.53 +		$(LOG)/HOL-Hoare_Parallel.gz $(LOG)/HOL-Lex.gz		\
    1.54  		$(LOG)/HOL-Algebra.gz $(LOG)/HOL-Auth.gz		\
    1.55  		$(LOG)/HOL-UNITY.gz $(LOG)/HOL-Modelcheck.gz		\
    1.56  		$(LOG)/HOL-Lambda.gz $(LOG)/HOL-Bali.gz			\
isabelle