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-Fun HOL-Recdef \ |
7 default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Fun HOL-Fun \ |
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 |
102 $(LOG)/HOL-Fun.gz: $(OUT)/HOL Fun/ROOT.ML Fun/fun0.thy |
102 $(LOG)/HOL-Fun.gz: $(OUT)/HOL Fun/ROOT.ML Fun/fun0.thy |
103 $(USEDIR) Fun |
103 $(USEDIR) Fun |
104 @rm -f tutorial.dvi |
104 @rm -f tutorial.dvi |
105 |
105 |
106 |
106 |
107 ## HOL-Recdef |
|
108 |
|
109 HOL-Recdef: HOL $(LOG)/HOL-Recdef.gz |
|
110 |
|
111 $(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/ROOT.ML Recdef/examples.thy Recdef/termination.thy \ |
|
112 Recdef/simplification.thy Recdef/Induction.thy \ |
|
113 Recdef/Nested0.thy Recdef/Nested1.thy Recdef/Nested2.thy |
|
114 $(USEDIR) Recdef |
|
115 @rm -f tutorial.dvi |
|
116 |
|
117 |
|
118 ## HOL-Advanced |
107 ## HOL-Advanced |
119 |
108 |
120 HOL-Advanced: HOL $(LOG)/HOL-Advanced.gz |
109 HOL-Advanced: HOL $(LOG)/HOL-Advanced.gz |
121 |
110 |
122 $(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML Advanced/WFrec.thy \ |
111 $(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML |
123 Advanced/Partial.thy |
|
124 $(USEDIR) Advanced |
112 $(USEDIR) Advanced |
125 @rm -f tutorial.dvi |
113 @rm -f tutorial.dvi |
126 |
114 |
127 ## HOL-Rules |
115 ## HOL-Rules |
128 |
116 |
203 @rm -f tutorial.dvi |
191 @rm -f tutorial.dvi |
204 |
192 |
205 ## clean |
193 ## clean |
206 |
194 |
207 clean: |
195 clean: |
208 @rm -f tutorial.dvi $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Recdef.gz $(LOG)/HOL-Advanced.gz $(LOG)/HOL-Rules.gz $(LOG)/HOL-Sets.gz $(LOG)/HOL-CTL.gz $(LOG)/HOL-Inductive.gz $(LOG)/HOL-Types.gz $(LOG)/HOL-Protocol.gz $(LOG)/HOL-Documents.gz Rules/document/*.tex Sets/document/*.tex |
196 @rm -f tutorial.dvi $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Fun.gz $(LOG)/HOL-Advanced.gz $(LOG)/HOL-Rules.gz $(LOG)/HOL-Sets.gz $(LOG)/HOL-CTL.gz $(LOG)/HOL-Inductive.gz $(LOG)/HOL-Types.gz $(LOG)/HOL-Protocol.gz $(LOG)/HOL-Documents.gz Rules/document/*.tex Sets/document/*.tex |