| author | bulwahn | 
| Thu, 12 Jul 2012 16:22:33 +0200 | |
| changeset 48253 | 4410a709913c | 
| 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: 
25258diff
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: 
31676diff
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: 
25258diff
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: 
11857diff
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: 
11617diff
changeset | 229 | ## HOL-Documents | 
| 
0538cb0f7999
initial setup for chapter on document preparation;
 wenzelm parents: 
11617diff
changeset | 230 | |
| 
0538cb0f7999
initial setup for chapter on document preparation;
 wenzelm parents: 
11617diff
changeset | 231 | HOL-Documents: HOL $(LOG)/HOL-Documents.gz | 
| 
0538cb0f7999
initial setup for chapter on document preparation;
 wenzelm parents: 
11617diff
changeset | 232 | |
| 
0538cb0f7999
initial setup for chapter on document preparation;
 wenzelm parents: 
11617diff
changeset | 233 | $(LOG)/HOL-Documents.gz: $(OUT)/HOL Documents/Documents.thy Documents/ROOT.ML | 
| 
0538cb0f7999
initial setup for chapter on document preparation;
 wenzelm parents: 
11617diff
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: 
11617diff
changeset | 239 | @rm -f tutorial.dvi | 
| 
0538cb0f7999
initial setup for chapter on document preparation;
 wenzelm parents: 
11617diff
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: 
25258diff
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 |