16 |
14 |
17 SRC = $(ISABELLE_HOME)/src |
15 SRC = $(ISABELLE_HOME)/src |
18 OUT = $(ISABELLE_OUTPUT) |
16 OUT = $(ISABELLE_OUTPUT) |
19 LOG = $(OUT)/log |
17 LOG = $(OUT)/log |
20 OPTIONS = -m brackets -i true -d "" -D document -M 1 |
18 OPTIONS = -m brackets -i true -d "" -D document -M 1 |
21 USEDIR = @$(ISABELLE_TOOL) usedir $(OPTIONS) $(OUT)/HOL |
19 USEDIR = @$(ISABELLE_TOOL) usedir $(OPTIONS) |
22 |
20 |
23 |
21 |
24 ## HOL |
22 ## HOL |
25 |
23 |
26 HOL: |
24 HOL: |
27 @cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL |
25 @cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL |
28 |
26 |
29 |
27 |
|
28 ## HOL-Tutorial |
30 |
29 |
31 ## HOL-Ifexpr |
30 HOL-Tutorial: HOL $(LOG)/HOL-Tutorial.gz |
32 |
31 |
33 HOL-Ifexpr: HOL $(LOG)/HOL-Ifexpr.gz |
32 $(LOG)/HOL-Tutorial.gz: $(OUT)/HOL ROOT.ML Ifexpr/Ifexpr.thy \ |
|
33 ToyList2/ToyList.thy CodeGen/CodeGen.thy Datatype/ABexpr.thy \ |
|
34 Datatype/Nested.thy Datatype/unfoldnested.thy Datatype/Fundata.thy \ |
|
35 Trie/Trie.thy Fun/fun0.thy Advanced/simp2.thy Rules/Basic.thy \ |
|
36 Rules/Blast.thy Rules/Force.thy Rules/Primes.thy Rules/Forward.thy \ |
|
37 Rules/Tacticals.thy Rules/find2.thy Sets/Examples.thy \ |
|
38 Sets/Functions.thy Sets/Recur.thy Sets/Relations.thy CTL/Base.thy \ |
|
39 CTL/PDL.thy CTL/CTL.thy CTL/CTLind.thy Inductive/Even.thy \ |
|
40 Inductive/Mutual.thy Inductive/Star.thy Inductive/AB.thy \ |
|
41 Inductive/Advanced.thy Types/Numbers.thy Types/Pairs.thy \ |
|
42 Types/Records.thy Types/Typedefs.thy Types/Overloading.thy \ |
|
43 Types/Axioms.thy Misc/Tree.thy Misc/Tree2.thy Misc/Plus.thy \ |
|
44 Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/Option2.thy \ |
|
45 Misc/types.thy Misc/prime_def.thy Misc/case_exprs.thy Misc/simp.thy \ |
|
46 Misc/Itrev.thy Misc/AdvancedInd.thy Misc/appendix.thy \ |
|
47 Protocol/Message.thy Protocol/Event.thy Protocol/Public.thy \ |
|
48 Protocol/NS_Public.thy Documents/Documents.thy |
|
49 $(USEDIR) -s Tutorial $(OUT)/HOL . |
34 |
50 |
35 $(LOG)/HOL-Ifexpr.gz: $(OUT)/HOL Ifexpr/Ifexpr.thy Ifexpr/ROOT.ML |
|
36 $(USEDIR) Ifexpr |
|
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 |
|
41 @rm -f tutorial.dvi |
|
42 |
51 |
43 ## HOL-ToyList |
52 ## HOL-ToyList2 |
44 |
53 |
45 HOL-ToyList: HOL $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz |
54 HOL-ToyList2: HOL $(LOG)/HOL-ToyList2.gz |
46 |
55 |
47 ToyList2/ToyList.thy: ToyList2/ToyList1 ToyList2/ToyList2 |
56 ToyList2/ToyList.thy: ToyList2/ToyList1 ToyList2/ToyList2 |
48 cat ToyList2/ToyList1 ToyList2/ToyList2 > ToyList2/ToyList.thy |
57 cat ToyList2/ToyList1 ToyList2/ToyList2 > ToyList2/ToyList.thy |
49 |
58 |
50 $(LOG)/HOL-ToyList2.gz: $(OUT)/HOL ToyList2/ToyList.thy ToyList2/ROOT.ML |
59 $(LOG)/HOL-ToyList2.gz: $(OUT)/HOL ToyList2/ROOT.ML |
51 $(USEDIR) ToyList2 |
60 $(USEDIR) $(OUT)/HOL ToyList2 |
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 |
|
56 @rm -f tutorial.dvi |
|
57 |
61 |
58 $(LOG)/HOL-ToyList.gz: $(OUT)/HOL ToyList/ToyList.thy ToyList/ROOT.ML |
|
59 $(USEDIR) ToyList |
|
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 |
|
64 @rm -f tutorial.dvi |
|
65 |
|
66 ## HOL-CodeGen |
|
67 |
|
68 HOL-CodeGen: HOL $(LOG)/HOL-CodeGen.gz |
|
69 |
|
70 $(LOG)/HOL-CodeGen.gz: $(OUT)/HOL CodeGen/ROOT.ML CodeGen/CodeGen.thy |
|
71 $(USEDIR) CodeGen |
|
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 |
|
76 @rm -f tutorial.dvi |
|
77 |
|
78 |
|
79 ## HOL-Datatype |
|
80 |
|
81 HOL-Datatype: HOL $(LOG)/HOL-Datatype.gz |
|
82 |
|
83 $(LOG)/HOL-Datatype.gz: $(OUT)/HOL Datatype/ROOT.ML Datatype/ABexpr.thy \ |
|
84 Datatype/Nested.thy Datatype/unfoldnested.thy \ |
|
85 Datatype/Fundata.thy |
|
86 $(USEDIR) Datatype |
|
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 |
|
91 @rm -f tutorial.dvi |
|
92 |
|
93 |
|
94 ## HOL-Trie |
|
95 |
|
96 HOL-Trie: HOL $(LOG)/HOL-Trie.gz |
|
97 |
|
98 $(LOG)/HOL-Trie.gz: $(OUT)/HOL Trie/ROOT.ML Trie/Trie.thy |
|
99 $(USEDIR) Trie |
|
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 |
|
104 @rm -f tutorial.dvi |
|
105 |
|
106 |
|
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 |
|
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 |
|
117 @rm -f tutorial.dvi |
|
118 |
|
119 |
|
120 ## HOL-Advanced |
|
121 |
|
122 HOL-Advanced: HOL $(LOG)/HOL-Advanced.gz |
|
123 |
|
124 $(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp2.thy Advanced/ROOT.ML |
|
125 $(USEDIR) Advanced |
|
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 |
|
130 @rm -f tutorial.dvi |
|
131 |
|
132 ## HOL-Rules |
|
133 |
|
134 HOL-Rules: HOL $(LOG)/HOL-Rules.gz |
|
135 |
|
136 $(LOG)/HOL-Rules.gz: $(OUT)/HOL Rules/Basic.thy \ |
|
137 Rules/Blast.thy Rules/Force.thy Rules/Primes.thy Rules/Forward.thy \ |
|
138 Rules/Tacticals.thy Rules/find2.thy Rules/ROOT.ML |
|
139 @$(USEDIR) Rules |
|
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 |
|
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 |
|
152 @$(USEDIR) Sets |
|
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 |
|
157 @rm -f tutorial.dvi |
|
158 |
|
159 ## HOL-CTL |
|
160 |
|
161 HOL-CTL: HOL $(LOG)/HOL-CTL.gz |
|
162 |
|
163 $(LOG)/HOL-CTL.gz: $(OUT)/HOL CTL/Base.thy CTL/PDL.thy CTL/CTL.thy CTL/CTLind.thy CTL/ROOT.ML |
|
164 $(USEDIR) CTL |
|
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 |
|
169 @rm -f tutorial.dvi |
|
170 |
|
171 ## HOL-Inductive |
|
172 |
|
173 HOL-Inductive: HOL $(LOG)/HOL-Inductive.gz |
|
174 |
|
175 $(LOG)/HOL-Inductive.gz: $(OUT)/HOL Inductive/ROOT.ML \ |
|
176 Inductive/Even.thy Inductive/Mutual.thy Inductive/Star.thy Inductive/AB.thy \ |
|
177 Inductive/Advanced.thy |
|
178 $(USEDIR) Inductive |
|
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 |
|
183 @rm -f tutorial.dvi |
|
184 |
|
185 ## HOL-Types |
|
186 |
|
187 HOL-Types: HOL $(LOG)/HOL-Types.gz |
|
188 |
|
189 $(LOG)/HOL-Types.gz: $(OUT)/HOL Types/ROOT.ML \ |
|
190 Types/Numbers.thy Types/Pairs.thy Types/Records.thy Types/Typedefs.thy \ |
|
191 Types/Overloading.thy Types/Axioms.thy |
|
192 $(USEDIR) Types |
|
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 |
|
197 @rm -f tutorial.dvi |
|
198 |
|
199 ## HOL-Misc |
|
200 |
|
201 HOL-Misc: HOL $(LOG)/HOL-Misc.gz |
|
202 |
|
203 $(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \ |
|
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 \ |
|
206 Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy Misc/appendix.thy |
|
207 $(USEDIR) Misc |
|
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 |
|
212 @rm -f tutorial.dvi |
|
213 |
|
214 |
|
215 ## HOL-Protocol |
|
216 |
|
217 HOL-Protocol: HOL $(LOG)/HOL-Protocol.gz |
|
218 |
|
219 $(LOG)/HOL-Protocol.gz: $(OUT)/HOL Protocol/ROOT.ML \ |
|
220 Protocol/Message.thy Protocol/Event.thy \ |
|
221 Protocol/Public.thy Protocol/NS_Public.thy |
|
222 $(USEDIR) Protocol |
|
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 |
|
227 @rm -f tutorial.dvi |
|
228 |
|
229 ## HOL-Documents |
|
230 |
|
231 HOL-Documents: HOL $(LOG)/HOL-Documents.gz |
|
232 |
|
233 $(LOG)/HOL-Documents.gz: $(OUT)/HOL Documents/Documents.thy Documents/ROOT.ML |
|
234 $(USEDIR) Documents |
|
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 |
|
239 @rm -f tutorial.dvi |
|
240 |
62 |
241 ## clean |
63 ## clean |
242 |
64 |
243 clean: |
65 clean: |
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 |
66 @rm -f tutorial.dvi $(LOG)/HOL-Tutorial.gz $(LOG)/HOL-ToyList2.gz |