548 $(LOG)/HOL-IMPP.gz: $(OUT)/HOL IMPP/ROOT.ML IMPP/Com.thy \ |
553 $(LOG)/HOL-IMPP.gz: $(OUT)/HOL IMPP/ROOT.ML IMPP/Com.thy \ |
549 IMPP/Natural.thy IMPP/Hoare.thy IMPP/Misc.thy IMPP/EvenOdd.thy |
554 IMPP/Natural.thy IMPP/Hoare.thy IMPP/Misc.thy IMPP/EvenOdd.thy |
550 @$(ISABELLE_TOOL) usedir $(OUT)/HOL IMPP |
555 @$(ISABELLE_TOOL) usedir $(OUT)/HOL IMPP |
551 |
556 |
552 |
557 |
553 ## HOL-Import |
558 ## Import sessions |
554 |
559 |
555 IMPORTER_FILES = \ |
560 Import-HOL4: $(OUT)/Import-HOL4 |
556 Import/HOL4Compat.thy \ |
561 |
557 Import/HOLLightCompat.thy Import/HOL4Setup.thy Import/HOL4Syntax.thy \ |
562 $(OUT)/Import-HOL4: $(OUT)/HOL \ |
558 Import/MakeEqual.thy Import/ROOT.ML Import/hol4rews.ML \ |
563 Import/HOL4/ROOT.ML \ |
559 Import/import.ML Import/import_syntax.ML \ |
564 Import/HOL4/Compatibility.thy |
560 Import/proof_kernel.ML Import/replay.ML Import/shuffler.ML \ |
565 @cd Import/HOL4; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL Import-HOL4 |
561 Library/ContNotDenum.thy Old_Number_Theory/Primes.thy |
566 |
562 |
567 Import-HOL_Light: $(OUT)/Import-HOL_Light |
563 HOL-Import: HOL $(LOG)/HOL-Import.gz |
568 |
564 |
569 $(OUT)/Import-HOL_Light: $(OUT)/HOL \ |
565 $(LOG)/HOL-Import.gz: $(OUT)/HOL $(IMPORTER_FILES) |
570 Import/HOL_Light/ROOT.ML \ |
566 @$(ISABELLE_TOOL) usedir -p 0 $(OUT)/HOL Import |
571 Import/HOL_Light/Compatibility.thy |
567 |
572 @cd Import/HOL_Light; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL Import-HOL_Light |
568 |
573 |
569 ## HOL-Generate-HOL |
574 Import-HOL4-Imported: $(OUT)/Import-HOL4-Imported |
570 |
575 |
571 HOL-Generate-HOL: HOL $(LOG)/HOL-Generate-HOL.gz |
576 $(OUT)/Import-HOL4-Imported: $(OUT)/Import-HOL4 \ |
572 |
577 Import/HOL4/imported.ML \ |
573 $(LOG)/HOL-Generate-HOL.gz: $(OUT)/HOL \ |
578 Import/HOL4/Imported.thy |
574 $(IMPORTER_FILES) Import/Generate-HOL/GenHOL4Base.thy \ |
579 @cd Import/HOL4; $(ISABELLE_TOOL) usedir -b -f imported.ML -p 0 $(OUT)/Import-HOL4 Import-HOL4-Imported |
575 Import/Generate-HOL/GenHOL4Prob.thy \ |
580 |
576 Import/Generate-HOL/GenHOL4Real.thy \ |
581 Import-HOL_Light-Imported: $(OUT)/Import-HOL_Light-Imported |
577 Import/Generate-HOL/GenHOL4Vec.thy \ |
582 |
578 Import/Generate-HOL/GenHOL4Word32.thy Import/Generate-HOL/ROOT.ML |
583 $(OUT)/Import-HOL_Light-Imported: $(OUT)/Import-HOL_Light \ |
579 @cd Import; $(ISABELLE_TOOL) usedir $(OUT)/HOL Generate-HOL |
584 Import/HOL_Light/imported.ML \ |
580 |
585 Import/HOL_Light/Imported.thy |
581 |
586 @cd Import/HOL_Light; $(ISABELLE_TOOL) usedir -b -f imported.ML -p 0 $(OUT)/Import-HOL_Light Import-HOL_Light-Imported |
582 ## HOL-Generate-HOLLight |
587 |
583 |
588 Import-HOL4-Generate: $(LOG)/Import-HOL4-Generate.gz |
584 HOL-Generate-HOLLight: HOL $(LOG)/HOL-Generate-HOLLight.gz |
589 |
585 |
590 $(LOG)/Import-HOL4-Generate.gz: $(OUT)/Import-HOL4 \ |
586 $(LOG)/HOL-Generate-HOLLight.gz: $(OUT)/HOL \ |
591 Import/HOL4/generate.ML \ |
587 $(IMPORTER_FILES) Import/Generate-HOLLight/GenHOLLight.thy \ |
592 Import/HOL4/Generate.thy |
588 Import/Generate-HOLLight/ROOT.ML |
593 @cd Import; $(ISABELLE_TOOL) usedir -f generate.ML -s Generate -p 0 $(OUT)/Import-HOL4 HOL4 |
589 @cd Import; $(ISABELLE_TOOL) usedir $(OUT)/HOL Generate-HOLLight |
594 |
590 |
595 Import-HOL_Light-Generate: $(LOG)/Import-HOL_Light-Generate.gz |
591 |
596 |
592 ## HOL-Import-HOL |
597 $(LOG)/Import-HOL_Light-Generate.gz: $(OUT)/Import-HOL_Light \ |
593 |
598 Import/HOL_Light/generate.ML \ |
594 HOL4: HOL $(LOG)/HOL4.gz |
599 Import/HOL_Light/Generate.thy |
595 |
600 @cd Import; $(ISABELLE_TOOL) usedir -f generate.ML -s Generate -p 0 $(OUT)/Import-HOL_Light HOL_Light |
596 HOL_IMPORT_FILES = arithmetic.imp bits.imp boolean_sequence.imp bool.imp \ |
|
597 bword_arith.imp bword_bitop.imp bword_num.imp combin.imp divides.imp \ |
|
598 hrat.imp hreal.imp ind_type.imp lim.imp list.imp marker.imp nets.imp \ |
|
599 numeral.imp num.imp one.imp operator.imp option.imp pair.imp poly.imp \ |
|
600 powser.imp pred_set.imp prime.imp prim_rec.imp prob_algebra.imp \ |
|
601 prob_canon.imp prob_extra.imp prob.imp prob_indep.imp prob_pseudo.imp \ |
|
602 prob_uniform.imp realax.imp real.imp relation.imp res_quan.imp \ |
|
603 rich_list.imp \ |
|
604 seq.imp state_transformer.imp sum.imp topology.imp transc.imp word32.imp \ |
|
605 word_base.imp word_bitop.imp word_num.imp |
|
606 |
|
607 $(LOG)/HOL4.gz: $(OUT)/HOL $(IMPORTER_FILES) \ |
|
608 $(HOL_IMPORT_FILES:%=Import/HOL/%) Import/HOL/HOL4Base.thy \ |
|
609 Import/HOL/HOL4Prob.thy Import/HOL/HOL4Real.thy \ |
|
610 Import/HOL/HOL4Vec.thy Import/HOL/HOL4Word32.thy Import/HOL/HOL4.thy \ |
|
611 Import/HOL/ROOT.ML |
|
612 @cd Import/HOL; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOL4 |
|
613 |
|
614 HOLLight: HOL $(LOG)/HOLLight.gz |
|
615 |
|
616 $(LOG)/HOLLight.gz: $(OUT)/HOL $(IMPORTER_FILES) \ |
|
617 Import/HOLLight/hollight.imp Import/HOLLight/HOLLight.thy \ |
|
618 Import/HOLLight/ROOT.ML |
|
619 @cd Import/HOLLight; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOLLight |
|
620 |
601 |
621 |
602 |
622 ## HOL-Number_Theory |
603 ## HOL-Number_Theory |
623 |
604 |
624 HOL-Number_Theory: HOL $(LOG)/HOL-Number_Theory.gz |
605 HOL-Number_Theory: HOL $(LOG)/HOL-Number_Theory.gz |