equal
deleted
inserted
replaced
19 HOL-CTL \ |
19 HOL-CTL \ |
20 HOL-GroupTheory \ |
20 HOL-GroupTheory \ |
21 HOL-Real-HahnBanach \ |
21 HOL-Real-HahnBanach \ |
22 HOL-Real-ex \ |
22 HOL-Real-ex \ |
23 HOL-Hoare \ |
23 HOL-Hoare \ |
|
24 HOL-HoareParallel \ |
24 HOL-IMP \ |
25 HOL-IMP \ |
25 HOL-IMPP \ |
26 HOL-IMPP \ |
26 HOL-IOA \ |
27 HOL-IOA \ |
27 HOL-Induct \ |
28 HOL-Induct \ |
28 HOL-Isar_examples \ |
29 HOL-Isar_examples \ |
284 Hoare/Examples.ML Hoare/Examples.thy Hoare/Hoare.ML Hoare/Hoare.thy \ |
285 Hoare/Examples.ML Hoare/Examples.thy Hoare/Hoare.ML Hoare/Hoare.thy \ |
285 Hoare/ROOT.ML |
286 Hoare/ROOT.ML |
286 @$(ISATOOL) usedir $(OUT)/HOL Hoare |
287 @$(ISATOOL) usedir $(OUT)/HOL Hoare |
287 |
288 |
288 |
289 |
|
290 ## HOL-HoareParallel |
|
291 |
|
292 HOL-HoareParallel: HOL $(LOG)/HOL-HoareParallel.gz |
|
293 |
|
294 $(LOG)/HOL-HoareParallel.gz: $(OUT)/HOL HoareParallel/Gar_Coll.thy \ |
|
295 HoareParallel/Graph.thy HoareParallel/Mul_Gar_Coll.thy \ |
|
296 HoareParallel/OG_Com.thy HoareParallel/OG_Examples.thy \ |
|
297 HoareParallel/OG_Hoare.thy HoareParallel/OG_Syntax.thy \ |
|
298 HoareParallel/OG_Tactics.thy HoareParallel/OG_Tran.thy \ |
|
299 HoareParallel/RG_Com.thy HoareParallel/RG_Examples.thy \ |
|
300 HoareParallel/RG_Hoare.thy HoareParallel/RG_Syntax.thy \ |
|
301 HoareParallel/RG_Tran.thy HoareParallel/ROOT.ML \ |
|
302 HoareParallel/document/root.tex |
|
303 @$(ISATOOL) usedir $(OUT)/HOL HoareParallel |
|
304 |
|
305 |
289 ## HOL-Lex |
306 ## HOL-Lex |
290 |
307 |
291 HOL-Lex: HOL $(LOG)/HOL-Lex.gz |
308 HOL-Lex: HOL $(LOG)/HOL-Lex.gz |
292 |
309 |
293 $(LOG)/HOL-Lex.gz: $(OUT)/HOL \ |
310 $(LOG)/HOL-Lex.gz: $(OUT)/HOL \ |
623 @rm -f $(OUT)/HOL $(OUT)/HOL-Real $(OUT)/HOL-Hyperreal $(OUT)/TLA \ |
640 @rm -f $(OUT)/HOL $(OUT)/HOL-Real $(OUT)/HOL-Hyperreal $(OUT)/TLA \ |
624 $(LOG)/HOL.gz $(LOG)/HOL-Real.gz $(LOG)/TLA.gz \ |
641 $(LOG)/HOL.gz $(LOG)/HOL-Real.gz $(LOG)/TLA.gz \ |
625 $(LOG)/HOL-Isar_examples.gz $(LOG)/HOL-Induct.gz \ |
642 $(LOG)/HOL-Isar_examples.gz $(LOG)/HOL-Induct.gz \ |
626 $(LOG)/HOL-ex.gz $(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz \ |
643 $(LOG)/HOL-ex.gz $(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz \ |
627 $(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz \ |
644 $(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz \ |
|
645 $(LOG)/HOL-HoareParallel.gz \ |
628 $(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz \ |
646 $(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz \ |
629 $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \ |
647 $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \ |
630 $(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \ |
648 $(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \ |
631 $(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz \ |
649 $(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz \ |
632 $(LOG)/HOL-Bali.gz $(LOG)/HOL-CTL.gz \ |
650 $(LOG)/HOL-Bali.gz $(LOG)/HOL-CTL.gz \ |