equal
deleted
inserted
replaced
679 |
679 |
680 ## HOL-Metis_Examples |
680 ## HOL-Metis_Examples |
681 |
681 |
682 HOL-Metis_Examples: HOL $(LOG)/HOL-Metis_Examples.gz |
682 HOL-Metis_Examples: HOL $(LOG)/HOL-Metis_Examples.gz |
683 |
683 |
684 $(LOG)/HOL-Metis_Examples.gz: $(OUT)/HOL Metis_Examples/ROOT.ML \ |
684 $(LOG)/HOL-Metis_Examples.gz: $(OUT)/HOL Metis_Examples/ROOT.ML \ |
685 Metis_Examples/Abstraction.thy Metis_Examples/BigO.thy \ |
685 Metis_Examples/Abstraction.thy Metis_Examples/BigO.thy \ |
686 Metis_Examples/BT.thy Metis_Examples/Message.thy \ |
686 Metis_Examples/BT.thy Metis_Examples/HO_Reas.thy \ |
687 Metis_Examples/Tarski.thy Metis_Examples/TransClosure.thy \ |
687 Metis_Examples/Message.thy Metis_Examples/Tarski.thy \ |
688 Metis_Examples/set.thy |
688 Metis_Examples/TransClosure.thy Metis_Examples/set.thy |
689 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Metis_Examples |
689 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Metis_Examples |
690 |
690 |
691 |
691 |
692 ## HOL-Nitpick_Examples |
692 ## HOL-Nitpick_Examples |
693 |
693 |