| author | wenzelm | 
| Fri, 16 Mar 2012 22:31:19 +0100 | |
| changeset 46973 | d68798000e46 | 
| parent 42512 | f1ca2b0e0265 | 
| child 48506 | af1dabad14c0 | 
| permissions | -rw-r--r-- | 
| 8743 | 1  | 
#  | 
2  | 
# IsaMakefile for Tutorial  | 
|
3  | 
#  | 
|
4  | 
||
5  | 
## targets  | 
|
6  | 
||
| 
25281
 
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
 
nipkow 
parents: 
25258 
diff
changeset
 | 
7  | 
default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Fun HOL-Fun \  | 
| 27423 | 8  | 
HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive HOL-Types HOL-Misc \  | 
| 42512 | 9  | 
HOL-Protocol HOL-Documents  | 
| 9520 | 10  | 
images:  | 
11  | 
test:  | 
|
12  | 
all: default  | 
|
| 8743 | 13  | 
|
14  | 
||
15  | 
## global settings  | 
|
16  | 
||
17  | 
SRC = $(ISABELLE_HOME)/src  | 
|
18  | 
OUT = $(ISABELLE_OUTPUT)  | 
|
19  | 
LOG = $(OUT)/log  | 
|
| 
32835
 
00c14c4a6b4f
enable slow-motion mode to accomodate unsynchronized refs within theory sources;
 
wenzelm 
parents: 
31676 
diff
changeset
 | 
20  | 
OPTIONS = -m brackets -i true -d "" -D document -M 1  | 
| 28500 | 21  | 
USEDIR = @$(ISABELLE_TOOL) usedir $(OPTIONS) $(OUT)/HOL  | 
| 11617 | 22  | 
|
| 8743 | 23  | 
|
24  | 
## HOL  | 
|
25  | 
||
26  | 
HOL:  | 
|
| 28500 | 27  | 
@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL  | 
| 8743 | 28  | 
|
29  | 
||
30  | 
||
31  | 
## HOL-Ifexpr  | 
|
32  | 
||
33  | 
HOL-Ifexpr: HOL $(LOG)/HOL-Ifexpr.gz  | 
|
34  | 
||
35  | 
$(LOG)/HOL-Ifexpr.gz: $(OUT)/HOL Ifexpr/Ifexpr.thy Ifexpr/ROOT.ML  | 
|
| 10676 | 36  | 
$(USEDIR) Ifexpr  | 
| 42512 | 37  | 
@rm -f Ifexpr/document/isabelle.sty  | 
38  | 
@rm -f Ifexpr/document/isabellesym.sty  | 
|
39  | 
@rm -f Ifexpr/document/pdfsetup.sty  | 
|
40  | 
@rm -f Ifexpr/document/session.tex  | 
|
| 8754 | 41  | 
@rm -f tutorial.dvi  | 
| 8743 | 42  | 
|
43  | 
## HOL-ToyList  | 
|
44  | 
||
45  | 
HOL-ToyList: HOL $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz  | 
|
46  | 
||
47  | 
ToyList2/ToyList.thy: ToyList2/ToyList1 ToyList2/ToyList2  | 
|
48  | 
cat ToyList2/ToyList1 ToyList2/ToyList2 > ToyList2/ToyList.thy  | 
|
49  | 
||
50  | 
$(LOG)/HOL-ToyList2.gz: $(OUT)/HOL ToyList2/ToyList.thy ToyList2/ROOT.ML  | 
|
| 10676 | 51  | 
$(USEDIR) ToyList2  | 
| 42512 | 52  | 
@rm -f ToyList2/document/isabelle.sty  | 
53  | 
@rm -f ToyList2/document/isabellesym.sty  | 
|
54  | 
@rm -f ToyList2/document/pdfsetup.sty  | 
|
55  | 
@rm -f ToyList2/document/session.tex  | 
|
| 8754 | 56  | 
@rm -f tutorial.dvi  | 
| 8743 | 57  | 
|
58  | 
$(LOG)/HOL-ToyList.gz: $(OUT)/HOL ToyList/ToyList.thy ToyList/ROOT.ML  | 
|
| 10676 | 59  | 
$(USEDIR) ToyList  | 
| 42512 | 60  | 
@rm -f ToyList/document/isabelle.sty  | 
61  | 
@rm -f ToyList/document/isabellesym.sty  | 
|
62  | 
@rm -f ToyList/document/pdfsetup.sty  | 
|
63  | 
@rm -f ToyList/document/session.tex  | 
|
| 8754 | 64  | 
@rm -f tutorial.dvi  | 
| 8743 | 65  | 
|
66  | 
## HOL-CodeGen  | 
|
67  | 
||
68  | 
HOL-CodeGen: HOL $(LOG)/HOL-CodeGen.gz  | 
|
69  | 
||
| 10676 | 70  | 
$(LOG)/HOL-CodeGen.gz: $(OUT)/HOL CodeGen/ROOT.ML CodeGen/CodeGen.thy  | 
71  | 
$(USEDIR) CodeGen  | 
|
| 42512 | 72  | 
@rm -f CodeGen/document/isabelle.sty  | 
73  | 
@rm -f CodeGen/document/isabellesym.sty  | 
|
74  | 
@rm -f CodeGen/document/pdfsetup.sty  | 
|
75  | 
@rm -f CodeGen/document/session.tex  | 
|
| 8754 | 76  | 
@rm -f tutorial.dvi  | 
| 8743 | 77  | 
|
78  | 
||
79  | 
## HOL-Datatype  | 
|
80  | 
||
81  | 
HOL-Datatype: HOL $(LOG)/HOL-Datatype.gz  | 
|
82  | 
||
| 8751 | 83  | 
$(LOG)/HOL-Datatype.gz: $(OUT)/HOL Datatype/ROOT.ML Datatype/ABexpr.thy \  | 
| 9666 | 84  | 
Datatype/Nested.thy Datatype/unfoldnested.thy \  | 
| 9644 | 85  | 
Datatype/Fundata.thy  | 
| 10676 | 86  | 
$(USEDIR) Datatype  | 
| 42512 | 87  | 
@rm -f Datatype/document/isabelle.sty  | 
88  | 
@rm -f Datatype/document/isabellesym.sty  | 
|
89  | 
@rm -f Datatype/document/pdfsetup.sty  | 
|
90  | 
@rm -f Datatype/document/session.tex  | 
|
| 8754 | 91  | 
@rm -f tutorial.dvi  | 
| 8743 | 92  | 
|
93  | 
||
94  | 
## HOL-Trie  | 
|
95  | 
||
96  | 
HOL-Trie: HOL $(LOG)/HOL-Trie.gz  | 
|
97  | 
||
| 10543 | 98  | 
$(LOG)/HOL-Trie.gz: $(OUT)/HOL Trie/ROOT.ML Trie/Trie.thy  | 
| 10676 | 99  | 
$(USEDIR) Trie  | 
| 42512 | 100  | 
@rm -f Trie/document/isabelle.sty  | 
101  | 
@rm -f Trie/document/isabellesym.sty  | 
|
102  | 
@rm -f Trie/document/pdfsetup.sty  | 
|
103  | 
@rm -f Trie/document/session.tex  | 
|
| 8754 | 104  | 
@rm -f tutorial.dvi  | 
| 8743 | 105  | 
|
106  | 
||
| 25258 | 107  | 
## HOL-Fun  | 
108  | 
||
109  | 
HOL-Fun: HOL $(LOG)/HOL-Fun.gz  | 
|
110  | 
||
111  | 
$(LOG)/HOL-Fun.gz: $(OUT)/HOL Fun/ROOT.ML Fun/fun0.thy  | 
|
112  | 
$(USEDIR) Fun  | 
|
| 42512 | 113  | 
@rm -f Fun/document/isabelle.sty  | 
114  | 
@rm -f Fun/document/isabellesym.sty  | 
|
115  | 
@rm -f Fun/document/pdfsetup.sty  | 
|
116  | 
@rm -f Fun/document/session.tex  | 
|
| 25258 | 117  | 
@rm -f tutorial.dvi  | 
118  | 
||
119  | 
||
| 9933 | 120  | 
## HOL-Advanced  | 
121  | 
||
122  | 
HOL-Advanced: HOL $(LOG)/HOL-Advanced.gz  | 
|
123  | 
||
| 
25281
 
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
 
nipkow 
parents: 
25258 
diff
changeset
 | 
124  | 
$(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML  | 
| 10676 | 125  | 
$(USEDIR) Advanced  | 
| 42512 | 126  | 
@rm -f Advanced/document/isabelle.sty  | 
127  | 
@rm -f Advanced/document/isabellesym.sty  | 
|
128  | 
@rm -f Advanced/document/pdfsetup.sty  | 
|
129  | 
@rm -f Advanced/document/session.tex  | 
|
| 9933 | 130  | 
@rm -f tutorial.dvi  | 
131  | 
||
| 10296 | 132  | 
## HOL-Rules  | 
133  | 
||
134  | 
HOL-Rules: HOL $(LOG)/HOL-Rules.gz  | 
|
135  | 
||
136  | 
$(LOG)/HOL-Rules.gz: $(OUT)/HOL Rules/Basic.thy \  | 
|
| 10956 | 137  | 
Rules/Blast.thy Rules/Force.thy Rules/Primes.thy Rules/Forward.thy \  | 
| 16543 | 138  | 
Rules/Tacticals.thy Rules/find2.thy Rules/ROOT.ML  | 
| 10840 | 139  | 
@$(USEDIR) Rules  | 
| 42512 | 140  | 
@rm -f Rules/document/isabelle.sty  | 
141  | 
@rm -f Rules/document/isabellesym.sty  | 
|
142  | 
@rm -f Rules/document/pdfsetup.sty  | 
|
143  | 
@rm -f Rules/document/session.tex  | 
|
| 10296 | 144  | 
@rm -f tutorial.dvi  | 
145  | 
||
146  | 
## HOL-Sets  | 
|
147  | 
||
148  | 
HOL-Sets: HOL $(LOG)/HOL-Sets.gz  | 
|
149  | 
||
150  | 
$(LOG)/HOL-Sets.gz: $(OUT)/HOL Sets/Examples.thy Sets/Functions.thy \  | 
|
151  | 
Sets/Recur.thy Sets/Relations.thy Sets/ROOT.ML  | 
|
| 10840 | 152  | 
@$(USEDIR) Sets  | 
| 42512 | 153  | 
@rm -f Sets/document/isabelle.sty  | 
154  | 
@rm -f Sets/document/isabellesym.sty  | 
|
155  | 
@rm -f Sets/document/pdfsetup.sty  | 
|
156  | 
@rm -f Sets/document/session.tex  | 
|
| 10296 | 157  | 
@rm -f tutorial.dvi  | 
158  | 
||
| 9958 | 159  | 
## HOL-CTL  | 
160  | 
||
161  | 
HOL-CTL: HOL $(LOG)/HOL-CTL.gz  | 
|
162  | 
||
| 10212 | 163  | 
$(LOG)/HOL-CTL.gz: $(OUT)/HOL CTL/Base.thy CTL/PDL.thy CTL/CTL.thy CTL/CTLind.thy CTL/ROOT.ML  | 
| 10676 | 164  | 
$(USEDIR) CTL  | 
| 42512 | 165  | 
@rm -f CTL/document/isabelle.sty  | 
166  | 
@rm -f CTL/document/isabellesym.sty  | 
|
167  | 
@rm -f CTL/document/pdfsetup.sty  | 
|
168  | 
@rm -f CTL/document/session.tex  | 
|
| 9958 | 169  | 
@rm -f tutorial.dvi  | 
170  | 
||
| 10217 | 171  | 
## HOL-Inductive  | 
172  | 
||
173  | 
HOL-Inductive: HOL $(LOG)/HOL-Inductive.gz  | 
|
174  | 
||
| 10225 | 175  | 
$(LOG)/HOL-Inductive.gz: $(OUT)/HOL Inductive/ROOT.ML \  | 
| 10762 | 176  | 
Inductive/Even.thy Inductive/Mutual.thy Inductive/Star.thy Inductive/AB.thy \  | 
177  | 
Inductive/Advanced.thy  | 
|
| 10676 | 178  | 
$(USEDIR) Inductive  | 
| 42512 | 179  | 
@rm -f Inductive/document/isabelle.sty  | 
180  | 
@rm -f Inductive/document/isabellesym.sty  | 
|
181  | 
@rm -f Inductive/document/pdfsetup.sty  | 
|
182  | 
@rm -f Inductive/document/session.tex  | 
|
| 10217 | 183  | 
@rm -f tutorial.dvi  | 
184  | 
||
| 10328 | 185  | 
## HOL-Types  | 
186  | 
||
| 27423 | 187  | 
HOL-Types: HOL $(LOG)/HOL-Types.gz  | 
| 10328 | 188  | 
|
| 27423 | 189  | 
$(LOG)/HOL-Types.gz: $(OUT)/HOL Types/ROOT.ML \  | 
| 
11858
 
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
 
wenzelm 
parents: 
11857 
diff
changeset
 | 
190  | 
Types/Numbers.thy Types/Pairs.thy Types/Records.thy Types/Typedefs.thy \  | 
| 10328 | 191  | 
Types/Overloading.thy Types/Axioms.thy  | 
| 27423 | 192  | 
$(USEDIR) Types  | 
| 42512 | 193  | 
@rm -f Types/document/isabelle.sty  | 
194  | 
@rm -f Types/document/isabellesym.sty  | 
|
195  | 
@rm -f Types/document/pdfsetup.sty  | 
|
196  | 
@rm -f Types/document/session.tex  | 
|
| 10328 | 197  | 
@rm -f tutorial.dvi  | 
198  | 
||
| 8743 | 199  | 
## HOL-Misc  | 
200  | 
||
201  | 
HOL-Misc: HOL $(LOG)/HOL-Misc.gz  | 
|
202  | 
||
| 9722 | 203  | 
$(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \  | 
| 13305 | 204  | 
Misc/Plus.thy Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy \  | 
205  | 
Misc/Option2.thy Misc/types.thy Misc/prime_def.thy Misc/case_exprs.thy \  | 
|
| 10978 | 206  | 
Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy Misc/appendix.thy  | 
| 10676 | 207  | 
$(USEDIR) Misc  | 
| 42512 | 208  | 
@rm -f Misc/document/isabelle.sty  | 
209  | 
@rm -f Misc/document/isabellesym.sty  | 
|
210  | 
@rm -f Misc/document/pdfsetup.sty  | 
|
211  | 
@rm -f Misc/document/session.tex  | 
|
| 8754 | 212  | 
@rm -f tutorial.dvi  | 
| 8743 | 213  | 
|
214  | 
||
| 11249 | 215  | 
## HOL-Protocol  | 
216  | 
||
217  | 
HOL-Protocol: HOL $(LOG)/HOL-Protocol.gz  | 
|
218  | 
||
219  | 
$(LOG)/HOL-Protocol.gz: $(OUT)/HOL Protocol/ROOT.ML \  | 
|
| 23926 | 220  | 
Protocol/Message.thy Protocol/Event.thy \  | 
221  | 
Protocol/Public.thy Protocol/NS_Public.thy  | 
|
| 11249 | 222  | 
$(USEDIR) Protocol  | 
| 42512 | 223  | 
@rm -f Protocol/document/isabelle.sty  | 
224  | 
@rm -f Protocol/document/isabellesym.sty  | 
|
225  | 
@rm -f Protocol/document/pdfsetup.sty  | 
|
226  | 
@rm -f Protocol/document/session.tex  | 
|
| 11249 | 227  | 
@rm -f tutorial.dvi  | 
228  | 
||
| 
11647
 
0538cb0f7999
initial setup for chapter on document preparation;
 
wenzelm 
parents: 
11617 
diff
changeset
 | 
229  | 
## HOL-Documents  | 
| 
 
0538cb0f7999
initial setup for chapter on document preparation;
 
wenzelm 
parents: 
11617 
diff
changeset
 | 
230  | 
|
| 
 
0538cb0f7999
initial setup for chapter on document preparation;
 
wenzelm 
parents: 
11617 
diff
changeset
 | 
231  | 
HOL-Documents: HOL $(LOG)/HOL-Documents.gz  | 
| 
 
0538cb0f7999
initial setup for chapter on document preparation;
 
wenzelm 
parents: 
11617 
diff
changeset
 | 
232  | 
|
| 
 
0538cb0f7999
initial setup for chapter on document preparation;
 
wenzelm 
parents: 
11617 
diff
changeset
 | 
233  | 
$(LOG)/HOL-Documents.gz: $(OUT)/HOL Documents/Documents.thy Documents/ROOT.ML  | 
| 
 
0538cb0f7999
initial setup for chapter on document preparation;
 
wenzelm 
parents: 
11617 
diff
changeset
 | 
234  | 
$(USEDIR) Documents  | 
| 42512 | 235  | 
@rm -f Documents/document/isabelle.sty  | 
236  | 
@rm -f Documents/document/isabellesym.sty  | 
|
237  | 
@rm -f Documents/document/pdfsetup.sty  | 
|
238  | 
@rm -f Documents/document/session.tex  | 
|
| 
11647
 
0538cb0f7999
initial setup for chapter on document preparation;
 
wenzelm 
parents: 
11617 
diff
changeset
 | 
239  | 
@rm -f tutorial.dvi  | 
| 
 
0538cb0f7999
initial setup for chapter on document preparation;
 
wenzelm 
parents: 
11617 
diff
changeset
 | 
240  | 
|
| 8743 | 241  | 
## clean  | 
242  | 
||
243  | 
clean:  | 
|
| 
25281
 
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
 
nipkow 
parents: 
25258 
diff
changeset
 | 
244  | 
@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  |