234 IMPP/Natural.thy IMPP/Natural.ML IMPP/Hoare.thy IMPP/Hoare.ML \ |
235 IMPP/Natural.thy IMPP/Natural.ML IMPP/Hoare.thy IMPP/Hoare.ML \ |
235 IMPP/Misc.thy IMPP/Misc.ML IMPP/EvenOdd.thy IMPP/EvenOdd.ML |
236 IMPP/Misc.thy IMPP/Misc.ML IMPP/EvenOdd.thy IMPP/EvenOdd.ML |
236 @$(ISATOOL) usedir $(OUT)/HOL IMPP |
237 @$(ISATOOL) usedir $(OUT)/HOL IMPP |
237 |
238 |
238 |
239 |
|
240 ## HOL-Complex-Import |
|
241 |
|
242 IMPORTER_FILES = Import/proof_kernel.ML Import/replay.ML \ |
|
243 Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \ |
|
244 Import/HOL4Syntax.thy Import/HOL4Compat.thy Import/import_syntax.ML \ |
|
245 Import/hol4rews.ML Import/import_package.ML Import/ROOT.ML |
|
246 |
|
247 HOL-Complex-Import: HOL-Complex $(LOG)/HOL-Complex-Import.gz |
|
248 |
|
249 $(LOG)/HOL-Complex-Import.gz: $(OUT)/HOL-Complex $(IMPORTER_FILES) |
|
250 @$(ISATOOL) usedir $(OUT)/HOL-Complex Import |
|
251 |
|
252 |
|
253 ## HOL-Complex-Generate-HOL |
|
254 |
|
255 HOL-Complex-Generate-HOL: HOL-Complex $(LOG)/HOL-Complex-Generate-HOL.gz |
|
256 |
|
257 $(LOG)/HOL-Complex-Generate-HOL.gz: $(OUT)/HOL-Complex $(IMPORTER_FILES) \ |
|
258 Import/Generate-HOL/GenHOL4Base.thy Import/Generate-HOL/GenHOL4Prob.thy \ |
|
259 Import/Generate-HOL/GenHOL4Real.thy Import/Generate-HOL/GenHOL4Vec.thy \ |
|
260 Import/Generate-HOL/GenHOL4Word32.thy Import/Generate-HOL/ROOT.ML |
|
261 @cd Import; $(ISATOOL) usedir $(OUT)/HOL-Complex Generate-HOL |
|
262 |
|
263 |
|
264 ## HOL-Import-HOL |
|
265 |
|
266 HOL-Import-HOL: HOL-Complex $(LOG)/HOL-Import-HOL.gz |
|
267 |
|
268 HOL_IMPORT_FILES = arithmetic.imp bits.imp boolean_sequence.imp bool.imp \ |
|
269 bword_arith.imp bword_bitop.imp bword_num.imp combin.imp divides.imp \ |
|
270 hrat.imp hreal.imp ind_type.imp lim.imp list.imp marker.imp nets.imp \ |
|
271 numeral.imp num.imp one.imp operator.imp option.imp pair.imp poly.imp \ |
|
272 powser.imp pred_set.imp prime.imp prim_rec.imp prob_algebra.imp \ |
|
273 prob_canon.imp prob_extra.imp prob.imp prob_indep.imp prob_pseudo.imp \ |
|
274 prob_uniform.imp realax.imp real.imp relation.imp res_quan.imp rich_list.imp \ |
|
275 seq.imp state_transformer.imp sum.imp topology.imp transc.imp word32.imp \ |
|
276 word_base.imp word_bitop.imp word_num.imp |
|
277 |
|
278 $(LOG)/HOL-Import-HOL.gz: $(OUT)/HOL-Complex $(IMPORTER_FILES) \ |
|
279 $(HOL_IMPORT_FILES:%=Import/HOL/%) Import/HOL/HOL4Base.thy \ |
|
280 Import/HOL/HOL4Prob.thy Import/HOL/HOL4Real.thy Import/HOL/HOL4Vec.thy \ |
|
281 Import/HOL/HOL4Word32.thy Import/HOL/HOL4.thy Import/HOL/ROOT.ML |
|
282 @cd Import/HOL; $(ISATOOL) usedir -b $(OUT)/HOL-Complex HOL-Import-HOL |
|
283 |
|
284 |
239 ## HOL-NumberTheory |
285 ## HOL-NumberTheory |
240 |
286 |
241 HOL-NumberTheory: HOL $(LOG)/HOL-NumberTheory.gz |
287 HOL-NumberTheory: HOL $(LOG)/HOL-NumberTheory.gz |
242 |
288 |
243 $(LOG)/HOL-NumberTheory.gz: $(OUT)/HOL \ |
289 $(LOG)/HOL-NumberTheory.gz: $(OUT)/HOL \ |