equal
deleted
inserted
replaced
68 HOL-Proofs-Lambda \ |
68 HOL-Proofs-Lambda \ |
69 HOL-SET_Protocol \ |
69 HOL-SET_Protocol \ |
70 HOL-SPARK-Examples \ |
70 HOL-SPARK-Examples \ |
71 HOL-Word-SMT_Examples \ |
71 HOL-Word-SMT_Examples \ |
72 HOL-Statespace \ |
72 HOL-Statespace \ |
73 HOL-Subst \ |
|
74 TLA-Buffer \ |
73 TLA-Buffer \ |
75 TLA-Inc \ |
74 TLA-Inc \ |
76 TLA-Memory \ |
75 TLA-Memory \ |
77 HOL-TPTP \ |
76 HOL-TPTP \ |
78 HOL-UNITY \ |
77 HOL-UNITY \ |
494 Hahn_Banach/Vector_Space.thy Hahn_Banach/Zorn_Lemma.thy \ |
493 Hahn_Banach/Vector_Space.thy Hahn_Banach/Zorn_Lemma.thy \ |
495 Hahn_Banach/document/root.bib Hahn_Banach/document/root.tex |
494 Hahn_Banach/document/root.bib Hahn_Banach/document/root.tex |
496 @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hahn_Banach |
495 @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hahn_Banach |
497 |
496 |
498 |
497 |
499 ## HOL-Subst |
|
500 |
|
501 HOL-Subst: HOL $(LOG)/HOL-Subst.gz |
|
502 |
|
503 $(LOG)/HOL-Subst.gz: $(OUT)/HOL Subst/AList.thy Subst/ROOT.ML \ |
|
504 Subst/Subst.thy Subst/UTerm.thy Subst/Unifier.thy Subst/Unify.thy |
|
505 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Subst |
|
506 |
|
507 |
|
508 ## HOL-Induct |
498 ## HOL-Induct |
509 |
499 |
510 HOL-Induct: HOL $(LOG)/HOL-Induct.gz |
500 HOL-Induct: HOL $(LOG)/HOL-Induct.gz |
511 |
501 |
512 $(LOG)/HOL-Induct.gz: $(OUT)/HOL Induct/Com.thy Induct/Comb.thy \ |
502 $(LOG)/HOL-Induct.gz: $(OUT)/HOL Induct/Com.thy Induct/Comb.thy \ |
1752 $(LOG)/HOL-Proofs.gz $(LOG)/HOL-Proofs-ex.gz \ |
1742 $(LOG)/HOL-Proofs.gz $(LOG)/HOL-Proofs-ex.gz \ |
1753 $(LOG)/HOL-Proofs-Extraction.gz \ |
1743 $(LOG)/HOL-Proofs-Extraction.gz \ |
1754 $(LOG)/HOL-Proofs-Lambda.gz $(LOG)/HOL-SET_Protocol.gz \ |
1744 $(LOG)/HOL-Proofs-Lambda.gz $(LOG)/HOL-SET_Protocol.gz \ |
1755 $(LOG)/HOL-Word-SMT_Examples.gz \ |
1745 $(LOG)/HOL-Word-SMT_Examples.gz \ |
1756 $(LOG)/HOL-SPARK.gz $(LOG)/HOL-SPARK-Examples.gz \ |
1746 $(LOG)/HOL-SPARK.gz $(LOG)/HOL-SPARK-Examples.gz \ |
1757 $(LOG)/HOL-Statespace.gz $(LOG)/HOL-Subst.gz \ |
1747 $(LOG)/HOL-Statespace.gz \ |
1758 $(LOG)/HOL-UNITY.gz $(LOG)/HOL-Unix.gz \ |
1748 $(LOG)/HOL-UNITY.gz $(LOG)/HOL-Unix.gz \ |
1759 $(LOG)/HOL-Word-Examples.gz $(LOG)/HOL-Word.gz \ |
1749 $(LOG)/HOL-Word-Examples.gz $(LOG)/HOL-Word.gz \ |
1760 $(LOG)/HOL-ZF.gz $(LOG)/HOL-ex.gz $(LOG)/HOL.gz \ |
1750 $(LOG)/HOL-ZF.gz $(LOG)/HOL-ex.gz $(LOG)/HOL.gz \ |
1761 $(LOG)/HOL4.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Inc.gz \ |
1751 $(LOG)/HOL4.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Inc.gz \ |
1762 $(LOG)/TLA-Memory.gz $(LOG)/TLA.gz $(OUT)/HOL \ |
1752 $(LOG)/TLA-Memory.gz $(LOG)/TLA.gz $(OUT)/HOL \ |