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-CTL HOL-Misc styles |
7 default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef HOL-Advanced HOL-CTL HOL-Inductive HOL-Misc styles |
8 images: |
8 images: |
9 test: |
9 test: |
10 all: default |
10 all: default |
11 |
11 |
12 |
12 |
108 |
108 |
109 $(LOG)/HOL-CTL.gz: $(OUT)/HOL CTL/Base.thy CTL/PDL.thy CTL/CTL.thy CTL/CTLind.thy CTL/ROOT.ML |
109 $(LOG)/HOL-CTL.gz: $(OUT)/HOL CTL/Base.thy CTL/PDL.thy CTL/CTL.thy CTL/CTLind.thy CTL/ROOT.ML |
110 @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL CTL |
110 @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL CTL |
111 @rm -f tutorial.dvi |
111 @rm -f tutorial.dvi |
112 |
112 |
|
113 ## HOL-Inductive |
|
114 |
|
115 HOL-Inductive: HOL $(LOG)/HOL-Inductive.gz |
|
116 |
|
117 $(LOG)/HOL-Inductive.gz: $(OUT)/HOL Inductive/AB.thy Inductive/ROOT.ML |
|
118 @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Inductive |
|
119 @rm -f tutorial.dvi |
|
120 |
113 ## HOL-Misc |
121 ## HOL-Misc |
114 |
122 |
115 HOL-Misc: HOL $(LOG)/HOL-Misc.gz |
123 HOL-Misc: HOL $(LOG)/HOL-Misc.gz |
116 |
124 |
117 $(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \ |
125 $(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \ |
124 |
132 |
125 |
133 |
126 ## clean |
134 ## clean |
127 |
135 |
128 clean: |
136 clean: |
129 @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-CTL.gz |
137 @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-CTL.gz $(LOG)/HOL-Inductive.gz |