equal
deleted
inserted
replaced
10 images: \ |
10 images: \ |
11 HOL \ |
11 HOL \ |
12 HOL-Library \ |
12 HOL-Library \ |
13 HOL-Algebra \ |
13 HOL-Algebra \ |
14 HOL-Boogie \ |
14 HOL-Boogie \ |
|
15 HOL-IMP \ |
15 HOL-Multivariate_Analysis \ |
16 HOL-Multivariate_Analysis \ |
16 HOL-NSA \ |
17 HOL-NSA \ |
17 HOL-Nominal \ |
18 HOL-Nominal \ |
18 HOL-Proofs \ |
19 HOL-Proofs \ |
19 HOL-SPARK \ |
20 HOL-SPARK \ |
37 HOLCF-FOCUS \ |
38 HOLCF-FOCUS \ |
38 HOLCF-IMP \ |
39 HOLCF-IMP \ |
39 HOLCF-Library \ |
40 HOLCF-Library \ |
40 HOLCF-Tutorial \ |
41 HOLCF-Tutorial \ |
41 HOLCF-ex \ |
42 HOLCF-ex \ |
42 HOL-IMP \ |
|
43 HOL-IMPP \ |
43 HOL-IMPP \ |
44 HOL-IOA \ |
44 HOL-IOA \ |
45 IOA-ABP \ |
45 IOA-ABP \ |
46 IOA-NTP \ |
46 IOA-NTP \ |
47 IOA-Storage \ |
47 IOA-Storage \ |
524 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Induct |
524 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Induct |
525 |
525 |
526 |
526 |
527 ## HOL-IMP |
527 ## HOL-IMP |
528 |
528 |
529 HOL-IMP: HOL $(LOG)/HOL-IMP.gz |
529 HOL-IMP: HOL $(OUT)/HOL-IMP |
530 |
530 |
531 $(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/ASM.thy IMP/AExp.thy IMP/BExp.thy \ |
531 $(OUT)/HOL-IMP: $(OUT)/HOL IMP/ASM.thy IMP/AExp.thy IMP/BExp.thy \ |
532 IMP/Big_Step.thy IMP/C_like.thy IMP/Com.thy IMP/Compiler.thy \ |
532 IMP/Big_Step.thy IMP/C_like.thy IMP/Com.thy IMP/Compiler.thy \ |
533 IMP/Comp_Rev.thy IMP/Def_Ass.thy IMP/Def_Ass_Big.thy IMP/Def_Ass_Exp.thy \ |
533 IMP/Comp_Rev.thy IMP/Def_Ass.thy IMP/Def_Ass_Big.thy IMP/Def_Ass_Exp.thy \ |
534 IMP/Def_Ass_Small.thy IMP/Def_Ass_Sound_Big.thy \ |
534 IMP/Def_Ass_Small.thy IMP/Def_Ass_Sound_Big.thy \ |
535 IMP/Def_Ass_Sound_Small.thy IMP/Denotation.thy IMP/Hoare.thy \ |
535 IMP/Def_Ass_Sound_Small.thy IMP/Denotation.thy IMP/Hoare.thy \ |
536 IMP/HoareT.thy IMP/Hoare_Examples.thy IMP/Hoare_Sound_Complete.thy \ |
536 IMP/HoareT.thy IMP/Hoare_Examples.thy IMP/Hoare_Sound_Complete.thy \ |
538 IMP/Procs_Dyn_Vars_Dyn.thy IMP/Procs_Stat_Vars_Dyn.thy \ |
538 IMP/Procs_Dyn_Vars_Dyn.thy IMP/Procs_Stat_Vars_Dyn.thy \ |
539 IMP/Procs_Stat_Vars_Stat.thy IMP/Sec_Type_Expr.thy IMP/Sec_Typing.thy \ |
539 IMP/Procs_Stat_Vars_Stat.thy IMP/Sec_Type_Expr.thy IMP/Sec_Typing.thy \ |
540 IMP/Sec_TypingT.thy IMP/Small_Step.thy IMP/Star.thy IMP/Types.thy \ |
540 IMP/Sec_TypingT.thy IMP/Small_Step.thy IMP/Star.thy IMP/Types.thy \ |
541 IMP/Util.thy IMP/VC.thy IMP/Vars.thy \ |
541 IMP/Util.thy IMP/VC.thy IMP/Vars.thy \ |
542 IMP/ROOT.ML IMP/document/root.tex IMP/document/root.bib |
542 IMP/ROOT.ML IMP/document/root.tex IMP/document/root.bib |
543 @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL IMP |
543 @cd IMP && $(ISABELLE_TOOL) usedir -g true -b $(OUT)/HOL HOL-IMP |
544 |
544 |
545 |
545 |
546 ## HOL-IMPP |
546 ## HOL-IMPP |
547 |
547 |
548 HOL-IMPP: HOL $(LOG)/HOL-IMPP.gz |
548 HOL-IMPP: HOL $(LOG)/HOL-IMPP.gz |
1770 $(LOG)/HOL-Word-Examples.gz $(LOG)/HOL-Word.gz \ |
1770 $(LOG)/HOL-Word-Examples.gz $(LOG)/HOL-Word.gz \ |
1771 $(LOG)/HOL-ZF.gz $(LOG)/HOL-ex.gz $(LOG)/HOL.gz \ |
1771 $(LOG)/HOL-ZF.gz $(LOG)/HOL-ex.gz $(LOG)/HOL.gz \ |
1772 $(LOG)/HOL4.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Inc.gz \ |
1772 $(LOG)/HOL4.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Inc.gz \ |
1773 $(LOG)/TLA-Memory.gz $(LOG)/TLA.gz $(OUT)/HOL \ |
1773 $(LOG)/TLA-Memory.gz $(LOG)/TLA.gz $(OUT)/HOL \ |
1774 $(OUT)/HOL-Algebra $(OUT)/HOL-Base $(OUT)/HOL-Boogie \ |
1774 $(OUT)/HOL-Algebra $(OUT)/HOL-Base $(OUT)/HOL-Boogie \ |
1775 $(OUT)/HOL-Main $(OUT)/HOL-Multivariate_Analysis \ |
1775 $(OUT)/HOL-IMP $(OUT)/HOL-Main $(OUT)/HOL-Multivariate_Analysis \ |
1776 $(OUT)/HOL-NSA $(OUT)/HOL-Nominal $(OUT)/HOL-Plain \ |
1776 $(OUT)/HOL-NSA $(OUT)/HOL-Nominal $(OUT)/HOL-Plain \ |
1777 $(OUT)/HOL-Probability $(OUT)/HOL-Proofs \ |
1777 $(OUT)/HOL-Probability $(OUT)/HOL-Proofs \ |
1778 $(OUT)/HOL-SPARK \ |
1778 $(OUT)/HOL-SPARK \ |
1779 $(OUT)/HOL-Word $(OUT)/HOL4 $(OUT)/TLA \ |
1779 $(OUT)/HOL-Word $(OUT)/HOL4 $(OUT)/TLA \ |
1780 $(OUT)/HOLCF $(LOG)/HOLCF.gz $(LOG)/HOLCF-IMP.gz \ |
1780 $(OUT)/HOLCF $(LOG)/HOLCF.gz $(LOG)/HOLCF-IMP.gz \ |