| author | haftmann | 
| Fri, 17 Aug 2007 13:58:59 +0200 | |
| changeset 24305 | b1df9e31cda1 | 
| parent 23926 | 391742a44617 | 
| child 25258 | 22d16596c306 | 
| permissions | -rw-r--r-- | 
| 8743 | 1  | 
#  | 
2  | 
# IsaMakefile for Tutorial  | 
|
3  | 
#  | 
|
4  | 
||
5  | 
## targets  | 
|
6  | 
||
| 
11647
 
0538cb0f7999
initial setup for chapter on document preparation;
 
wenzelm 
parents: 
11617 
diff
changeset
 | 
7  | 
default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef \  | 
| 13977 | 8  | 
HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive HOL-Complex-Types HOL-Misc \  | 
| 
11647
 
0538cb0f7999
initial setup for chapter on document preparation;
 
wenzelm 
parents: 
11617 
diff
changeset
 | 
9  | 
HOL-Protocol HOL-Documents styles  | 
| 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  | 
|
| 17055 | 20  | 
OPTIONS = -m brackets -i true -d "" -D document  | 
| 11617 | 21  | 
USEDIR = @$(ISATOOL) usedir $(OPTIONS) $(OUT)/HOL  | 
| 13977 | 22  | 
REALUSEDIR = @$(ISATOOL) usedir $(OPTIONS) $(OUT)/HOL-Complex  | 
| 11617 | 23  | 
|
| 8743 | 24  | 
|
25  | 
## HOL  | 
|
26  | 
||
27  | 
HOL:  | 
|
28  | 
@cd $(SRC)/HOL; $(ISATOOL) make HOL  | 
|
29  | 
||
| 13977 | 30  | 
HOL-Complex:  | 
31  | 
@cd $(SRC)/HOL; $(ISATOOL) make HOL-Complex  | 
|
| 10765 | 32  | 
|
| 
8825
 
0c9cf33d499b
improved handling of Isabelle styles (less garbage);
 
wenzelm 
parents: 
8754 
diff
changeset
 | 
33  | 
styles:  | 
| 10654 | 34  | 
@rm -f isabelle.sty  | 
35  | 
@rm -f isabellesym.sty  | 
|
36  | 
@rm -f pdfsetup.sty  | 
|
| 8847 | 37  | 
@$(ISATOOL) latex -o sty >/dev/null  | 
38  | 
@rm -f pdfsetup.sty  | 
|
| 
8825
 
0c9cf33d499b
improved handling of Isabelle styles (less garbage);
 
wenzelm 
parents: 
8754 
diff
changeset
 | 
39  | 
@rm -f */document/isabelle.sty  | 
| 
 
0c9cf33d499b
improved handling of Isabelle styles (less garbage);
 
wenzelm 
parents: 
8754 
diff
changeset
 | 
40  | 
@rm -f */document/isabellesym.sty  | 
| 
 
0c9cf33d499b
improved handling of Isabelle styles (less garbage);
 
wenzelm 
parents: 
8754 
diff
changeset
 | 
41  | 
@rm -f */document/pdfsetup.sty  | 
| 10002 | 42  | 
@rm -f */document/session.tex  | 
| 11401 | 43  | 
|
| 8743 | 44  | 
|
45  | 
||
46  | 
## HOL-Ifexpr  | 
|
47  | 
||
48  | 
HOL-Ifexpr: HOL $(LOG)/HOL-Ifexpr.gz  | 
|
49  | 
||
50  | 
$(LOG)/HOL-Ifexpr.gz: $(OUT)/HOL Ifexpr/Ifexpr.thy Ifexpr/ROOT.ML  | 
|
| 10676 | 51  | 
$(USEDIR) Ifexpr  | 
| 8754 | 52  | 
@rm -f tutorial.dvi  | 
| 8743 | 53  | 
|
54  | 
## HOL-ToyList  | 
|
55  | 
||
56  | 
HOL-ToyList: HOL $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz  | 
|
57  | 
||
58  | 
ToyList2/ToyList.thy: ToyList2/ToyList1 ToyList2/ToyList2  | 
|
59  | 
cat ToyList2/ToyList1 ToyList2/ToyList2 > ToyList2/ToyList.thy  | 
|
60  | 
||
61  | 
$(LOG)/HOL-ToyList2.gz: $(OUT)/HOL ToyList2/ToyList.thy ToyList2/ROOT.ML  | 
|
| 10676 | 62  | 
$(USEDIR) ToyList2  | 
| 8754 | 63  | 
@rm -f tutorial.dvi  | 
| 8743 | 64  | 
|
65  | 
$(LOG)/HOL-ToyList.gz: $(OUT)/HOL ToyList/ToyList.thy ToyList/ROOT.ML  | 
|
| 10676 | 66  | 
$(USEDIR) ToyList  | 
| 8754 | 67  | 
@rm -f tutorial.dvi  | 
| 8743 | 68  | 
|
69  | 
## HOL-CodeGen  | 
|
70  | 
||
71  | 
HOL-CodeGen: HOL $(LOG)/HOL-CodeGen.gz  | 
|
72  | 
||
| 10676 | 73  | 
$(LOG)/HOL-CodeGen.gz: $(OUT)/HOL CodeGen/ROOT.ML CodeGen/CodeGen.thy  | 
74  | 
$(USEDIR) CodeGen  | 
|
| 8754 | 75  | 
@rm -f tutorial.dvi  | 
| 8743 | 76  | 
|
77  | 
||
78  | 
## HOL-Datatype  | 
|
79  | 
||
80  | 
HOL-Datatype: HOL $(LOG)/HOL-Datatype.gz  | 
|
81  | 
||
| 8751 | 82  | 
$(LOG)/HOL-Datatype.gz: $(OUT)/HOL Datatype/ROOT.ML Datatype/ABexpr.thy \  | 
| 9666 | 83  | 
Datatype/Nested.thy Datatype/unfoldnested.thy \  | 
| 9644 | 84  | 
Datatype/Fundata.thy  | 
| 10676 | 85  | 
$(USEDIR) Datatype  | 
| 8754 | 86  | 
@rm -f tutorial.dvi  | 
| 8743 | 87  | 
|
88  | 
||
89  | 
## HOL-Trie  | 
|
90  | 
||
91  | 
HOL-Trie: HOL $(LOG)/HOL-Trie.gz  | 
|
92  | 
||
| 10543 | 93  | 
$(LOG)/HOL-Trie.gz: $(OUT)/HOL Trie/ROOT.ML Trie/Trie.thy  | 
| 10676 | 94  | 
$(USEDIR) Trie  | 
| 8754 | 95  | 
@rm -f tutorial.dvi  | 
| 8743 | 96  | 
|
97  | 
||
98  | 
## HOL-Recdef  | 
|
99  | 
||
100  | 
HOL-Recdef: HOL $(LOG)/HOL-Recdef.gz  | 
|
101  | 
||
| 10186 | 102  | 
$(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/ROOT.ML Recdef/examples.thy Recdef/termination.thy \  | 
| 9644 | 103  | 
Recdef/simplification.thy Recdef/Induction.thy \  | 
| 10187 | 104  | 
Recdef/Nested0.thy Recdef/Nested1.thy Recdef/Nested2.thy  | 
| 10676 | 105  | 
$(USEDIR) Recdef  | 
| 8754 | 106  | 
@rm -f tutorial.dvi  | 
| 8743 | 107  | 
|
108  | 
||
| 9933 | 109  | 
## HOL-Advanced  | 
110  | 
||
111  | 
HOL-Advanced: HOL $(LOG)/HOL-Advanced.gz  | 
|
112  | 
||
| 10654 | 113  | 
$(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML Advanced/WFrec.thy \  | 
114  | 
Advanced/Partial.thy  | 
|
| 10676 | 115  | 
$(USEDIR) Advanced  | 
| 9933 | 116  | 
@rm -f tutorial.dvi  | 
117  | 
||
| 10296 | 118  | 
## HOL-Rules  | 
119  | 
||
120  | 
HOL-Rules: HOL $(LOG)/HOL-Rules.gz  | 
|
121  | 
||
122  | 
$(LOG)/HOL-Rules.gz: $(OUT)/HOL Rules/Basic.thy \  | 
|
| 10956 | 123  | 
Rules/Blast.thy Rules/Force.thy Rules/Primes.thy Rules/Forward.thy \  | 
| 16543 | 124  | 
Rules/Tacticals.thy Rules/find2.thy Rules/ROOT.ML  | 
| 10840 | 125  | 
@$(USEDIR) Rules  | 
| 10296 | 126  | 
@rm -f tutorial.dvi  | 
127  | 
||
128  | 
## HOL-Sets  | 
|
129  | 
||
130  | 
HOL-Sets: HOL $(LOG)/HOL-Sets.gz  | 
|
131  | 
||
132  | 
$(LOG)/HOL-Sets.gz: $(OUT)/HOL Sets/Examples.thy Sets/Functions.thy \  | 
|
133  | 
Sets/Recur.thy Sets/Relations.thy Sets/ROOT.ML  | 
|
| 10840 | 134  | 
@$(USEDIR) Sets  | 
| 10296 | 135  | 
@rm -f tutorial.dvi  | 
136  | 
||
| 9958 | 137  | 
## HOL-CTL  | 
138  | 
||
139  | 
HOL-CTL: HOL $(LOG)/HOL-CTL.gz  | 
|
140  | 
||
| 10212 | 141  | 
$(LOG)/HOL-CTL.gz: $(OUT)/HOL CTL/Base.thy CTL/PDL.thy CTL/CTL.thy CTL/CTLind.thy CTL/ROOT.ML  | 
| 10676 | 142  | 
$(USEDIR) CTL  | 
| 9958 | 143  | 
@rm -f tutorial.dvi  | 
144  | 
||
| 10217 | 145  | 
## HOL-Inductive  | 
146  | 
||
147  | 
HOL-Inductive: HOL $(LOG)/HOL-Inductive.gz  | 
|
148  | 
||
| 10225 | 149  | 
$(LOG)/HOL-Inductive.gz: $(OUT)/HOL Inductive/ROOT.ML \  | 
| 10762 | 150  | 
Inductive/Even.thy Inductive/Mutual.thy Inductive/Star.thy Inductive/AB.thy \  | 
151  | 
Inductive/Advanced.thy  | 
|
| 10676 | 152  | 
$(USEDIR) Inductive  | 
| 10217 | 153  | 
@rm -f tutorial.dvi  | 
154  | 
||
| 10328 | 155  | 
## HOL-Types  | 
156  | 
||
| 13977 | 157  | 
HOL-Complex-Types: HOL-Complex $(LOG)/HOL-Complex-Types.gz  | 
| 10328 | 158  | 
|
| 13977 | 159  | 
$(LOG)/HOL-Complex-Types.gz: $(OUT)/HOL-Complex Types/ROOT.ML \  | 
| 
11858
 
ca128c9100b6
renamed Typedef.thy to Typedefs.thy (former already present in main HOL);
 
wenzelm 
parents: 
11857 
diff
changeset
 | 
160  | 
Types/Numbers.thy Types/Pairs.thy Types/Records.thy Types/Typedefs.thy \  | 
| 10328 | 161  | 
Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \  | 
162  | 
Types/Overloading.thy Types/Axioms.thy  | 
|
| 10765 | 163  | 
$(REALUSEDIR) Types  | 
| 10328 | 164  | 
@rm -f tutorial.dvi  | 
165  | 
||
| 8743 | 166  | 
## HOL-Misc  | 
167  | 
||
168  | 
HOL-Misc: HOL $(LOG)/HOL-Misc.gz  | 
|
169  | 
||
| 9722 | 170  | 
$(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \  | 
| 13305 | 171  | 
Misc/Plus.thy Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy \  | 
172  | 
Misc/Option2.thy Misc/types.thy Misc/prime_def.thy Misc/case_exprs.thy \  | 
|
| 10978 | 173  | 
Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy Misc/appendix.thy  | 
| 10676 | 174  | 
$(USEDIR) Misc  | 
| 8754 | 175  | 
@rm -f tutorial.dvi  | 
| 8743 | 176  | 
|
177  | 
||
| 11249 | 178  | 
## HOL-Protocol  | 
179  | 
||
180  | 
HOL-Protocol: HOL $(LOG)/HOL-Protocol.gz  | 
|
181  | 
||
182  | 
$(LOG)/HOL-Protocol.gz: $(OUT)/HOL Protocol/ROOT.ML \  | 
|
| 23926 | 183  | 
Protocol/Message.thy Protocol/Event.thy \  | 
184  | 
Protocol/Public.thy Protocol/NS_Public.thy  | 
|
| 11249 | 185  | 
$(USEDIR) Protocol  | 
186  | 
@rm -f tutorial.dvi  | 
|
187  | 
||
| 
11647
 
0538cb0f7999
initial setup for chapter on document preparation;
 
wenzelm 
parents: 
11617 
diff
changeset
 | 
188  | 
## HOL-Documents  | 
| 
 
0538cb0f7999
initial setup for chapter on document preparation;
 
wenzelm 
parents: 
11617 
diff
changeset
 | 
189  | 
|
| 
 
0538cb0f7999
initial setup for chapter on document preparation;
 
wenzelm 
parents: 
11617 
diff
changeset
 | 
190  | 
HOL-Documents: HOL $(LOG)/HOL-Documents.gz  | 
| 
 
0538cb0f7999
initial setup for chapter on document preparation;
 
wenzelm 
parents: 
11617 
diff
changeset
 | 
191  | 
|
| 
 
0538cb0f7999
initial setup for chapter on document preparation;
 
wenzelm 
parents: 
11617 
diff
changeset
 | 
192  | 
$(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
 | 
193  | 
$(USEDIR) Documents  | 
| 
 
0538cb0f7999
initial setup for chapter on document preparation;
 
wenzelm 
parents: 
11617 
diff
changeset
 | 
194  | 
@rm -f tutorial.dvi  | 
| 
 
0538cb0f7999
initial setup for chapter on document preparation;
 
wenzelm 
parents: 
11617 
diff
changeset
 | 
195  | 
|
| 8743 | 196  | 
## clean  | 
197  | 
||
198  | 
clean:  | 
|
| 
11647
 
0538cb0f7999
initial setup for chapter on document preparation;
 
wenzelm 
parents: 
11617 
diff
changeset
 | 
199  | 
@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  |