| author | wenzelm | 
| Thu, 19 Jul 2007 23:18:55 +0200 | |
| changeset 23868 | 8c6f2e7bfdb4 | 
| parent 17055 | eacce1cd716a | 
| child 23926 | 391742a44617 | 
| 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: 
11617diff
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: 
11617diff
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: 
8754diff
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: 
8754diff
changeset | 39 | @rm -f */document/isabelle.sty | 
| 
0c9cf33d499b
improved handling of Isabelle styles (less garbage);
 wenzelm parents: 
8754diff
changeset | 40 | @rm -f */document/isabellesym.sty | 
| 
0c9cf33d499b
improved handling of Isabelle styles (less garbage);
 wenzelm parents: 
8754diff
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: 
11857diff
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 \ | |
| 183 | Protocol/Message.thy Protocol/Message_lemmas.ML \ | |
| 184 | Protocol/Event.thy Protocol/Event_lemmas.ML \ | |
| 185 | Protocol/Public.thy Protocol/Public_lemmas.ML \ | |
| 186 | Protocol/NS_Public.thy | |
| 187 | $(USEDIR) Protocol | |
| 188 | @rm -f tutorial.dvi | |
| 189 | ||
| 11647 
0538cb0f7999
initial setup for chapter on document preparation;
 wenzelm parents: 
11617diff
changeset | 190 | ## HOL-Documents | 
| 
0538cb0f7999
initial setup for chapter on document preparation;
 wenzelm parents: 
11617diff
changeset | 191 | |
| 
0538cb0f7999
initial setup for chapter on document preparation;
 wenzelm parents: 
11617diff
changeset | 192 | HOL-Documents: HOL $(LOG)/HOL-Documents.gz | 
| 
0538cb0f7999
initial setup for chapter on document preparation;
 wenzelm parents: 
11617diff
changeset | 193 | |
| 
0538cb0f7999
initial setup for chapter on document preparation;
 wenzelm parents: 
11617diff
changeset | 194 | $(LOG)/HOL-Documents.gz: $(OUT)/HOL Documents/Documents.thy Documents/ROOT.ML | 
| 
0538cb0f7999
initial setup for chapter on document preparation;
 wenzelm parents: 
11617diff
changeset | 195 | $(USEDIR) Documents | 
| 
0538cb0f7999
initial setup for chapter on document preparation;
 wenzelm parents: 
11617diff
changeset | 196 | @rm -f tutorial.dvi | 
| 
0538cb0f7999
initial setup for chapter on document preparation;
 wenzelm parents: 
11617diff
changeset | 197 | |
| 8743 | 198 | ## clean | 
| 199 | ||
| 200 | clean: | |
| 11647 
0538cb0f7999
initial setup for chapter on document preparation;
 wenzelm parents: 
11617diff
changeset | 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 |