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 HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive HOL-Real-Types HOL-Misc HOL-Protocol styles |
7 default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef \ |
|
8 HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive HOL-Real-Types HOL-Misc \ |
|
9 HOL-Protocol HOL-Documents styles |
8 images: |
10 images: |
9 test: |
11 test: |
10 all: default |
12 all: default |
11 |
13 |
12 |
14 |
183 Protocol/Public.thy Protocol/Public_lemmas.ML \ |
185 Protocol/Public.thy Protocol/Public_lemmas.ML \ |
184 Protocol/NS_Public.thy |
186 Protocol/NS_Public.thy |
185 $(USEDIR) Protocol |
187 $(USEDIR) Protocol |
186 @rm -f tutorial.dvi |
188 @rm -f tutorial.dvi |
187 |
189 |
|
190 ## HOL-Documents |
|
191 |
|
192 HOL-Documents: HOL $(LOG)/HOL-Documents.gz |
|
193 |
|
194 $(LOG)/HOL-Documents.gz: $(OUT)/HOL Documents/Documents.thy Documents/ROOT.ML |
|
195 $(USEDIR) Documents |
|
196 @rm -f tutorial.dvi |
|
197 |
188 ## clean |
198 ## clean |
189 |
199 |
190 clean: |
200 clean: |
191 @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 Rules/document/*.tex Sets/document/*.tex |
201 @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 |