535 Hoare/HoareAbort.thy Hoare/SchorrWaite.thy Hoare/Separation.thy \ |
535 Hoare/HoareAbort.thy Hoare/SchorrWaite.thy Hoare/Separation.thy \ |
536 Hoare/SepLogHeap.thy Hoare/document/root.tex Hoare/document/root.bib |
536 Hoare/SepLogHeap.thy Hoare/document/root.tex Hoare/document/root.bib |
537 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Hoare |
537 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Hoare |
538 |
538 |
539 |
539 |
540 ## HOL-HoareParallel |
540 ## HOL-Hoare_Parallel |
541 |
541 |
542 HOL-HoareParallel: HOL $(LOG)/HOL-HoareParallel.gz |
542 HOL-Hoare_Parallel: HOL $(LOG)/HOL-Hoare_Parallel.gz |
543 |
543 |
544 $(LOG)/HOL-HoareParallel.gz: $(OUT)/HOL HoareParallel/Gar_Coll.thy \ |
544 $(LOG)/HOL-Hoare_Parallel.gz: $(OUT)/HOL Hoare_Parallel/Gar_Coll.thy \ |
545 HoareParallel/Graph.thy HoareParallel/Mul_Gar_Coll.thy \ |
545 Hoare_Parallel/Graph.thy Hoare_Parallel/Hoare_Parallel.thy \ |
546 HoareParallel/OG_Com.thy HoareParallel/OG_Examples.thy \ |
546 Hoare_Parallel/Mul_Gar_Coll.thy \ |
547 HoareParallel/OG_Hoare.thy HoareParallel/OG_Syntax.thy \ |
547 Hoare_Parallel/OG_Com.thy Hoare_Parallel/OG_Examples.thy \ |
548 HoareParallel/OG_Tactics.thy HoareParallel/OG_Tran.thy \ |
548 Hoare_Parallel/OG_Hoare.thy Hoare_Parallel/OG_Syntax.thy \ |
549 HoareParallel/Quote_Antiquote.thy HoareParallel/RG_Com.thy \ |
549 Hoare_Parallel/OG_Tactics.thy Hoare_Parallel/OG_Tran.thy \ |
550 HoareParallel/RG_Examples.thy HoareParallel/RG_Hoare.thy \ |
550 Hoare_Parallel/Quote_Antiquote.thy Hoare_Parallel/RG_Com.thy \ |
551 HoareParallel/RG_Syntax.thy HoareParallel/RG_Tran.thy \ |
551 Hoare_Parallel/RG_Examples.thy Hoare_Parallel/RG_Hoare.thy \ |
552 HoareParallel/ROOT.ML HoareParallel/document/root.tex \ |
552 Hoare_Parallel/RG_Syntax.thy Hoare_Parallel/RG_Tran.thy \ |
553 HoareParallel/document/root.bib |
553 Hoare_Parallel/ROOT.ML Hoare_Parallel/document/root.tex \ |
554 @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL HoareParallel |
554 Hoare_Parallel/document/root.bib |
|
555 @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hoare_Parallel |
555 |
556 |
556 |
557 |
557 ## HOL-MetisExamples |
558 ## HOL-MetisExamples |
558 |
559 |
559 HOL-MetisExamples: HOL $(LOG)/HOL-MetisExamples.gz |
560 HOL-MetisExamples: HOL $(LOG)/HOL-MetisExamples.gz |
1155 $(OUT)/HOL-Nominal $(OUT)/TLA $(LOG)/HOL.gz \ |
1156 $(OUT)/HOL-Nominal $(OUT)/TLA $(LOG)/HOL.gz \ |
1156 $(LOG)/TLA.gz $(LOG)/HOL-Isar_examples.gz \ |
1157 $(LOG)/TLA.gz $(LOG)/HOL-Isar_examples.gz \ |
1157 $(LOG)/HOL-Induct.gz $(LOG)/HOL-ex.gz \ |
1158 $(LOG)/HOL-Induct.gz $(LOG)/HOL-ex.gz \ |
1158 $(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz \ |
1159 $(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz \ |
1159 $(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz \ |
1160 $(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz \ |
1160 $(LOG)/HOL-HoareParallel.gz $(LOG)/HOL-Lex.gz \ |
1161 $(LOG)/HOL-Hoare_Parallel.gz $(LOG)/HOL-Lex.gz \ |
1161 $(LOG)/HOL-Algebra.gz $(LOG)/HOL-Auth.gz \ |
1162 $(LOG)/HOL-Algebra.gz $(LOG)/HOL-Auth.gz \ |
1162 $(LOG)/HOL-UNITY.gz $(LOG)/HOL-Modelcheck.gz \ |
1163 $(LOG)/HOL-UNITY.gz $(LOG)/HOL-Modelcheck.gz \ |
1163 $(LOG)/HOL-Lambda.gz $(LOG)/HOL-Bali.gz \ |
1164 $(LOG)/HOL-Lambda.gz $(LOG)/HOL-Bali.gz \ |
1164 $(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz \ |
1165 $(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz \ |
1165 $(LOG)/HOL-Nominal-Examples.gz $(LOG)/HOL-IOA.gz \ |
1166 $(LOG)/HOL-Nominal-Examples.gz $(LOG)/HOL-IOA.gz \ |