equal
deleted
inserted
replaced
4 |
4 |
5 ## targets |
5 ## targets |
6 |
6 |
7 default: HOL |
7 default: HOL |
8 generate: HOL-Generate-HOL HOL-Generate-HOLLight |
8 generate: HOL-Generate-HOL HOL-Generate-HOLLight |
9 images: HOL HOL-Base HOL-Plain HOL-Main HOL-Algebra HOL-Nominal HOL-NSA HOL-Word TLA HOL4 HOL-MicroJava |
9 images: HOL HOL-Base HOL-Plain HOL-Main HOL-Algebra HOL-Nominal HOL-NSA HOL-Word TLA HOL4 |
10 |
10 |
11 #Note: keep targets sorted (except for HOL-Library and HOL-ex) |
11 #Note: keep targets sorted (except for HOL-Library and HOL-ex) |
12 test: \ |
12 test: \ |
13 HOL-Library \ |
13 HOL-Library \ |
14 HOL-ex \ |
14 HOL-ex \ |
907 ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \ |
907 ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \ |
908 ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy \ |
908 ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy \ |
909 ex/Sudoku.thy ex/Tarski.thy \ |
909 ex/Sudoku.thy ex/Tarski.thy \ |
910 ex/Termination.thy ex/Transfer_Ex.thy ex/Unification.thy ex/document/root.bib \ |
910 ex/Termination.thy ex/Transfer_Ex.thy ex/Unification.thy ex/document/root.bib \ |
911 ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy \ |
911 ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy \ |
912 ex/Predicate_Compile.thy ex/predicate_compile.ML ex/Predicate_Compile_ex.thy |
912 ex/Predicate_Compile.thy Tools/Predicate_Compile/predicate_compile_core.ML ex/Predicate_Compile_ex.thy |
913 @$(ISABELLE_TOOL) usedir $(OUT)/HOL ex |
913 @$(ISABELLE_TOOL) usedir $(OUT)/HOL ex |
914 |
914 |
915 |
915 |
916 ## HOL-Isar_examples |
916 ## HOL-Isar_examples |
917 |
917 |