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-Trie HOL-Datatype HOL-Recdef \ |
7 default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Fun HOL-Recdef \ |
8 HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive HOL-Complex-Types HOL-Misc \ |
8 HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive HOL-Complex-Types HOL-Misc \ |
9 HOL-Protocol HOL-Documents styles |
9 HOL-Protocol HOL-Documents styles |
10 images: |
10 images: |
11 test: |
11 test: |
12 all: default |
12 all: default |
93 $(LOG)/HOL-Trie.gz: $(OUT)/HOL Trie/ROOT.ML Trie/Trie.thy |
93 $(LOG)/HOL-Trie.gz: $(OUT)/HOL Trie/ROOT.ML Trie/Trie.thy |
94 $(USEDIR) Trie |
94 $(USEDIR) Trie |
95 @rm -f tutorial.dvi |
95 @rm -f tutorial.dvi |
96 |
96 |
97 |
97 |
|
98 ## HOL-Fun |
|
99 |
|
100 HOL-Fun: HOL $(LOG)/HOL-Fun.gz |
|
101 |
|
102 $(LOG)/HOL-Fun.gz: $(OUT)/HOL Fun/ROOT.ML Fun/fun0.thy |
|
103 $(USEDIR) Fun |
|
104 @rm -f tutorial.dvi |
|
105 |
|
106 |
98 ## HOL-Recdef |
107 ## HOL-Recdef |
99 |
108 |
100 HOL-Recdef: HOL $(LOG)/HOL-Recdef.gz |
109 HOL-Recdef: HOL $(LOG)/HOL-Recdef.gz |
101 |
110 |
102 $(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/ROOT.ML Recdef/examples.thy Recdef/termination.thy \ |
111 $(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/ROOT.ML Recdef/examples.thy Recdef/termination.thy \ |