equal
deleted
inserted
replaced
2 # IsaMakefile for Tutorial |
2 # IsaMakefile for Tutorial |
3 # |
3 # |
4 |
4 |
5 ## targets |
5 ## targets |
6 |
6 |
7 default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Datatype HOL-Misc |
7 default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Datatype HOL-Recdef HOL-Misc |
8 |
8 |
9 |
9 |
10 ## global settings |
10 ## global settings |
11 |
11 |
12 SRC = $(ISABELLE_HOME)/src |
12 SRC = $(ISABELLE_HOME)/src |
87 Datatype/ROOT.ML Datatype/abgoalind.ML Datatype/autotac.ML \ |
87 Datatype/ROOT.ML Datatype/abgoalind.ML Datatype/autotac.ML \ |
88 Datatype/tidproof.ML Datatype/appmap.ML Datatype/lookupempty.ML \ |
88 Datatype/tidproof.ML Datatype/appmap.ML Datatype/lookupempty.ML \ |
89 Datatype/trieAdds.ML Datatype/triemain.ML Datatype/trieinduct.ML Datatype/trieexhaust.ML |
89 Datatype/trieAdds.ML Datatype/triemain.ML Datatype/trieinduct.ML Datatype/trieexhaust.ML |
90 @$(ISATOOL) usedir $(OUT)/HOL Datatype |
90 @$(ISATOOL) usedir $(OUT)/HOL Datatype |
91 |
91 |
|
92 ## HOL-Recdef |
|
93 |
|
94 HOL-Recdef: HOL $(LOG)/HOL-Recdef.gz |
|
95 |
|
96 Recdef/Examples.thy: Recdef/exprolog Recdef/fib Recdef/sep Recdef/last \ |
|
97 Recdef/constsgcd Recdef/gcd Recdef/ack |
|
98 cd Recdef; cat exprolog fib sep last constsgcd gcd ack end > Examples.thy |
|
99 |
|
100 Recdef/Sep1.thy: Recdef/sep1prolog Recdef/sep1 |
|
101 cd Recdef; cat sep1prolog sep1 end > Sep1.thy |
|
102 |
|
103 Recdef/Sep2.thy: Recdef/sep2prolog Recdef/sep2 |
|
104 cd Recdef; cat sep2prolog sep2 end > Sep2.thy |
|
105 |
|
106 $(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/ROOT.ML \ |
|
107 Recdef/Examples.thy Recdef/Sep1.thy Recdef/Sep2.thy |
|
108 @$(ISATOOL) usedir $(OUT)/HOL Recdef |
|
109 |
92 ## HOL-Misc |
110 ## HOL-Misc |
93 |
111 |
94 HOL-Misc: HOL $(LOG)/HOL-Misc.gz |
112 HOL-Misc: HOL $(LOG)/HOL-Misc.gz |
95 |
113 |
96 Misc/Tree.thy: Misc/treeprolog Misc/tree Misc/end |
114 Misc/Tree.thy: Misc/treeprolog Misc/tree Misc/end |