| author | wenzelm | 
| Mon, 31 Jul 2000 14:33:40 +0200 | |
| changeset 9480 | 7afb808b6b3e | 
| parent 8847 | d6c92979fa51 | 
| child 9493 | 494f8cd34df7 | 
| permissions | -rw-r--r-- | 
| 8743 | 1  | 
#  | 
2  | 
# IsaMakefile for Tutorial  | 
|
3  | 
#  | 
|
4  | 
||
5  | 
## targets  | 
|
6  | 
||
| 
8825
 
0c9cf33d499b
improved handling of Isabelle styles (less garbage);
 
wenzelm 
parents: 
8754 
diff
changeset
 | 
7  | 
default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef HOL-Misc styles  | 
| 8743 | 8  | 
|
9  | 
||
10  | 
## global settings  | 
|
11  | 
||
12  | 
SRC = $(ISABELLE_HOME)/src  | 
|
13  | 
OUT = $(ISABELLE_OUTPUT)  | 
|
14  | 
LOG = $(OUT)/log  | 
|
15  | 
||
16  | 
||
17  | 
## HOL  | 
|
18  | 
||
19  | 
HOL:  | 
|
20  | 
@cd $(SRC)/HOL; $(ISATOOL) make HOL  | 
|
21  | 
||
| 
8825
 
0c9cf33d499b
improved handling of Isabelle styles (less garbage);
 
wenzelm 
parents: 
8754 
diff
changeset
 | 
22  | 
styles:  | 
| 8847 | 23  | 
@$(ISATOOL) latex -o sty >/dev/null  | 
24  | 
@rm -f pdfsetup.sty  | 
|
| 
8825
 
0c9cf33d499b
improved handling of Isabelle styles (less garbage);
 
wenzelm 
parents: 
8754 
diff
changeset
 | 
25  | 
@rm -f */document/isabelle.sty  | 
| 
 
0c9cf33d499b
improved handling of Isabelle styles (less garbage);
 
wenzelm 
parents: 
8754 
diff
changeset
 | 
26  | 
@rm -f */document/isabellesym.sty  | 
| 
 
0c9cf33d499b
improved handling of Isabelle styles (less garbage);
 
wenzelm 
parents: 
8754 
diff
changeset
 | 
27  | 
@rm -f */document/pdfsetup.sty  | 
| 8743 | 28  | 
|
29  | 
||
30  | 
## HOL-Ifexpr  | 
|
31  | 
||
32  | 
HOL-Ifexpr: HOL $(LOG)/HOL-Ifexpr.gz  | 
|
33  | 
||
34  | 
$(LOG)/HOL-Ifexpr.gz: $(OUT)/HOL Ifexpr/Ifexpr.thy Ifexpr/ROOT.ML  | 
|
35  | 
@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Ifexpr  | 
|
| 8754 | 36  | 
@rm -f tutorial.dvi  | 
| 8743 | 37  | 
|
38  | 
## HOL-ToyList  | 
|
39  | 
||
40  | 
HOL-ToyList: HOL $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz  | 
|
41  | 
||
42  | 
ToyList2/ToyList.thy: ToyList2/ToyList1 ToyList2/ToyList2  | 
|
43  | 
cat ToyList2/ToyList1 ToyList2/ToyList2 > ToyList2/ToyList.thy  | 
|
44  | 
||
45  | 
$(LOG)/HOL-ToyList2.gz: $(OUT)/HOL ToyList2/ToyList.thy ToyList2/ROOT.ML  | 
|
46  | 
@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL ToyList2  | 
|
| 8754 | 47  | 
@rm -f tutorial.dvi  | 
| 8743 | 48  | 
|
49  | 
$(LOG)/HOL-ToyList.gz: $(OUT)/HOL ToyList/ToyList.thy ToyList/ROOT.ML  | 
|
50  | 
@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL ToyList  | 
|
| 8754 | 51  | 
@rm -f tutorial.dvi  | 
| 8743 | 52  | 
|
53  | 
## HOL-CodeGen  | 
|
54  | 
||
55  | 
HOL-CodeGen: HOL $(LOG)/HOL-CodeGen.gz  | 
|
56  | 
||
57  | 
$(LOG)/HOL-CodeGen.gz: $(OUT)/HOL CodeGen/CodeGen.thy  | 
|
58  | 
@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL CodeGen  | 
|
| 8754 | 59  | 
@rm -f tutorial.dvi  | 
| 8743 | 60  | 
|
61  | 
||
62  | 
## HOL-Datatype  | 
|
63  | 
||
64  | 
HOL-Datatype: HOL $(LOG)/HOL-Datatype.gz  | 
|
65  | 
||
| 8751 | 66  | 
$(LOG)/HOL-Datatype.gz: $(OUT)/HOL Datatype/ROOT.ML Datatype/ABexpr.thy \  | 
67  | 
Datatype/Nested.thy Datatype/unfoldnested.thy Datatype/Fundata.thy  | 
|
| 8743 | 68  | 
@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Datatype  | 
| 8754 | 69  | 
@rm -f tutorial.dvi  | 
| 8743 | 70  | 
|
71  | 
||
72  | 
## HOL-Trie  | 
|
73  | 
||
74  | 
HOL-Trie: HOL $(LOG)/HOL-Trie.gz  | 
|
75  | 
||
76  | 
$(LOG)/HOL-Trie.gz: $(OUT)/HOL Trie/Option2.thy Trie/Trie.thy  | 
|
77  | 
@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Trie  | 
|
| 8754 | 78  | 
@rm -f tutorial.dvi  | 
| 8743 | 79  | 
|
80  | 
||
81  | 
## HOL-Recdef  | 
|
82  | 
||
83  | 
HOL-Recdef: HOL $(LOG)/HOL-Recdef.gz  | 
|
84  | 
||
85  | 
$(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/examples.thy Recdef/termination.thy \  | 
|
86  | 
Recdef/simplification.thy Recdef/Induction.thy  | 
|
87  | 
@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Recdef  | 
|
| 8754 | 88  | 
@rm -f tutorial.dvi  | 
| 8743 | 89  | 
|
90  | 
||
91  | 
## HOL-Misc  | 
|
92  | 
||
93  | 
HOL-Misc: HOL $(LOG)/HOL-Misc.gz  | 
|
94  | 
||
95  | 
$(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/cases.thy \  | 
|
96  | 
Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/types.thy Misc/prime_def.thy \  | 
|
97  | 
Misc/arith1.thy Misc/arith2.thy Misc/arith3.thy Misc/arith4.thy \  | 
|
98  | 
Misc/def_rewr.thy Misc/let_rewr.thy Misc/cond_rewr.thy Misc/case_splits.thy \  | 
|
99  | 
Misc/trace_simp.thy Misc/Itrev.thy Misc/asm_simp.thy  | 
|
100  | 
@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Misc  | 
|
| 8754 | 101  | 
@rm -f tutorial.dvi  | 
| 8743 | 102  | 
|
103  | 
||
104  | 
## clean  | 
|
105  | 
||
106  | 
clean:  | 
|
| 8754 | 107  | 
@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  |