equal
deleted
inserted
replaced
13 test: \ |
13 test: \ |
14 HOL-Library \ |
14 HOL-Library \ |
15 HOL-Algebra \ |
15 HOL-Algebra \ |
16 HOL-Auth \ |
16 HOL-Auth \ |
17 HOL-AxClasses \ |
17 HOL-AxClasses \ |
18 HOL-BCV \ |
|
19 HOL-CTL \ |
18 HOL-CTL \ |
20 HOL-Real-HahnBanach \ |
19 HOL-Real-HahnBanach \ |
21 HOL-Real-ex \ |
20 HOL-Real-ex \ |
22 HOL-Hoare \ |
21 HOL-Hoare \ |
23 HOL-IMP \ |
22 HOL-IMP \ |
446 MicroJava/BV/Typing_Framework.thy MicroJava/BV/Typing_Framework_err.thy \ |
445 MicroJava/BV/Typing_Framework.thy MicroJava/BV/Typing_Framework_err.thy \ |
447 MicroJava/document/root.bib MicroJava/document/root.tex |
446 MicroJava/document/root.bib MicroJava/document/root.tex |
448 @$(ISATOOL) usedir $(OUT)/HOL MicroJava |
447 @$(ISATOOL) usedir $(OUT)/HOL MicroJava |
449 |
448 |
450 |
449 |
451 ## HOL-BCV |
|
452 |
|
453 HOL-BCV: HOL $(LOG)/HOL-BCV.gz |
|
454 |
|
455 $(LOG)/HOL-BCV.gz: $(OUT)/HOL \ |
|
456 BCV/DFA_Framework.thy BCV/DFA_Framework.ML BCV/Err.thy BCV/Err.ML \ |
|
457 BCV/JType.ML BCV/JType.thy BCV/JVM.ML BCV/JVM.thy \ |
|
458 BCV/Kildall.ML BCV/Kildall.thy BCV/Listn.ML BCV/Listn.thy \ |
|
459 BCV/Opt.ML BCV/Opt.thy BCV/ROOT.ML BCV/Semilat.ML BCV/Semilat.thy \ |
|
460 BCV/Product.ML BCV/Product.thy |
|
461 @$(ISATOOL) usedir $(OUT)/HOL BCV |
|
462 |
|
463 |
|
464 ## HOL-CTL |
450 ## HOL-CTL |
465 |
451 |
466 HOL-CTL: HOL $(LOG)/HOL-CTL.gz |
452 HOL-CTL: HOL $(LOG)/HOL-CTL.gz |
467 |
453 |
468 $(LOG)/HOL-CTL.gz: $(OUT)/HOL \ |
454 $(LOG)/HOL-CTL.gz: $(OUT)/HOL \ |
588 $(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz \ |
574 $(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz \ |
589 $(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz \ |
575 $(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz \ |
590 $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \ |
576 $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \ |
591 $(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \ |
577 $(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \ |
592 $(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz \ |
578 $(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz \ |
593 $(LOG)/HOL-BCV.gz $(LOG)/HOL-CTL.gz $(LOG)/HOL-MicroJava.gz \ |
579 $(LOG)/HOL-CTL.gz $(LOG)/HOL-MicroJava.gz \ |
594 $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \ |
580 $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \ |
595 $(LOG)/HOL-Lattice $(LOG)/HOL-Real-ex.gz \ |
581 $(LOG)/HOL-Lattice $(LOG)/HOL-Real-ex.gz \ |
596 $(LOG)/HOL-Real-HahnBanach.gz $(LOG)/TLA-Inc.gz \ |
582 $(LOG)/HOL-Real-HahnBanach.gz $(LOG)/TLA-Inc.gz \ |
597 $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz \ |
583 $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz \ |
598 $(LOG)/HOL-Library.gz $(LOG)/HOL-Unix.gz |
584 $(LOG)/HOL-Library.gz $(LOG)/HOL-Unix.gz |