equal
deleted
inserted
replaced
25 HOL-IOA \ |
25 HOL-IOA \ |
26 HOL-Induct \ |
26 HOL-Induct \ |
27 HOL-Isar_examples \ |
27 HOL-Isar_examples \ |
28 HOL-Lambda \ |
28 HOL-Lambda \ |
29 HOL-Lattice \ |
29 HOL-Lattice \ |
|
30 HOL-Matrix \ |
30 HOL-MetisExamples \ |
31 HOL-MetisExamples \ |
31 HOL-MicroJava \ |
32 HOL-MicroJava \ |
32 HOL-Modelcheck \ |
33 HOL-Modelcheck \ |
33 HOL-NanoJava \ |
34 HOL-NanoJava \ |
34 HOL-Nominal-Examples \ |
35 HOL-Nominal-Examples \ |
829 @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL SET-Protocol |
830 @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL SET-Protocol |
830 |
831 |
831 |
832 |
832 ## HOL-Matrix |
833 ## HOL-Matrix |
833 |
834 |
834 HOL-Matrix: HOL $(OUT)/HOL-Matrix |
835 HOL-Matrix: HOL $(LOG)/HOL-Matrix.gz |
835 |
836 |
836 $(OUT)/HOL-Matrix: $(OUT)/HOL \ |
837 $(LOG)/HOL-Matrix.gz: $(OUT)/HOL \ |
837 $(SRC)/Tools/Compute_Oracle/Compute_Oracle.thy \ |
838 $(SRC)/Tools/Compute_Oracle/Compute_Oracle.thy \ |
838 $(SRC)/Tools/Compute_Oracle/am_compiler.ML \ |
839 $(SRC)/Tools/Compute_Oracle/am_compiler.ML \ |
839 $(SRC)/Tools/Compute_Oracle/am_interpreter.ML \ |
840 $(SRC)/Tools/Compute_Oracle/am_interpreter.ML \ |
840 $(SRC)/Tools/Compute_Oracle/am.ML \ |
841 $(SRC)/Tools/Compute_Oracle/am.ML \ |
841 $(SRC)/Tools/Compute_Oracle/linker.ML \ |
842 $(SRC)/Tools/Compute_Oracle/linker.ML \ |