equal
deleted
inserted
replaced
46 HOL-Library-Codegenerator_Test \ |
46 HOL-Library-Codegenerator_Test \ |
47 HOL-Matrix \ |
47 HOL-Matrix \ |
48 HOL-Metis_Examples \ |
48 HOL-Metis_Examples \ |
49 HOL-MicroJava \ |
49 HOL-MicroJava \ |
50 HOL-Mirabelle \ |
50 HOL-Mirabelle \ |
51 HOL-Modelcheck \ |
|
52 HOL-Mutabelle \ |
51 HOL-Mutabelle \ |
53 HOL-NanoJava \ |
52 HOL-NanoJava \ |
54 HOL-Nitpick_Examples \ |
53 HOL-Nitpick_Examples \ |
55 HOL-Nominal-Examples \ |
54 HOL-Nominal-Examples \ |
56 HOL-Number_Theory \ |
55 HOL-Number_Theory \ |
792 $(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML ZF/LProd.thy \ |
791 $(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML ZF/LProd.thy \ |
793 ZF/HOLZF.thy ZF/MainZF.thy ZF/Games.thy ZF/document/root.tex |
792 ZF/HOLZF.thy ZF/MainZF.thy ZF/Games.thy ZF/document/root.tex |
794 @$(ISABELLE_TOOL) usedir $(OUT)/HOL ZF |
793 @$(ISABELLE_TOOL) usedir $(OUT)/HOL ZF |
795 |
794 |
796 |
795 |
797 ## HOL-Modelcheck |
|
798 |
|
799 HOL-Modelcheck: HOL $(LOG)/HOL-Modelcheck.gz |
|
800 |
|
801 $(LOG)/HOL-Modelcheck.gz: $(OUT)/HOL Modelcheck/CTL.thy \ |
|
802 Modelcheck/EindhovenExample.thy Modelcheck/EindhovenSyn.thy \ |
|
803 Modelcheck/MuCalculus.thy Modelcheck/MuckeExample1.thy \ |
|
804 Modelcheck/MuckeExample2.thy Modelcheck/MuckeSyn.thy \ |
|
805 Modelcheck/ROOT.ML Modelcheck/mucke_oracle.ML |
|
806 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Modelcheck |
|
807 |
|
808 |
|
809 ## HOL-Imperative_HOL |
796 ## HOL-Imperative_HOL |
810 |
797 |
811 HOL-Imperative_HOL: HOL $(LOG)/HOL-Imperative_HOL.gz |
798 HOL-Imperative_HOL: HOL $(LOG)/HOL-Imperative_HOL.gz |
812 |
799 |
813 $(LOG)/HOL-Imperative_HOL.gz: $(OUT)/HOL Imperative_HOL/Array.thy \ |
800 $(LOG)/HOL-Imperative_HOL.gz: $(OUT)/HOL Imperative_HOL/Array.thy \ |
1351 $(LOG)/HOL-Lattice $(LOG)/HOL-Lattice.gz \ |
1338 $(LOG)/HOL-Lattice $(LOG)/HOL-Lattice.gz \ |
1352 $(LOG)/HOL-Lex.gz $(LOG)/HOL-Library.gz \ |
1339 $(LOG)/HOL-Lex.gz $(LOG)/HOL-Library.gz \ |
1353 $(LOG)/HOL-Main.gz $(LOG)/HOL-Matrix \ |
1340 $(LOG)/HOL-Main.gz $(LOG)/HOL-Matrix \ |
1354 $(LOG)/HOL-Matrix.gz $(LOG)/HOL-Metis_Examples.gz \ |
1341 $(LOG)/HOL-Matrix.gz $(LOG)/HOL-Metis_Examples.gz \ |
1355 $(LOG)/HOL-MicroJava.gz $(LOG)/HOL-Mirabelle.gz \ |
1342 $(LOG)/HOL-MicroJava.gz $(LOG)/HOL-Mirabelle.gz \ |
1356 $(LOG)/HOL-Modelcheck.gz \ |
|
1357 $(LOG)/HOL-Multivariate_Analysis.gz \ |
1343 $(LOG)/HOL-Multivariate_Analysis.gz \ |
1358 $(LOG)/HOL-NSA-Examples.gz $(LOG)/HOL-NSA.gz \ |
1344 $(LOG)/HOL-NSA-Examples.gz $(LOG)/HOL-NSA.gz \ |
1359 $(LOG)/HOL-NanoJava.gz $(LOG)/HOL-Nitpick_Examples.gz \ |
1345 $(LOG)/HOL-NanoJava.gz $(LOG)/HOL-Nitpick_Examples.gz \ |
1360 $(LOG)/HOL-Nominal-Examples.gz $(LOG)/HOL-Nominal.gz \ |
1346 $(LOG)/HOL-Nominal-Examples.gz $(LOG)/HOL-Nominal.gz \ |
1361 $(LOG)/HOL-Number_Theory.gz \ |
1347 $(LOG)/HOL-Number_Theory.gz \ |