785 |
785 |
786 ## HOL-ZF |
786 ## HOL-ZF |
787 |
787 |
788 HOL-ZF: HOL $(LOG)/HOL-ZF.gz |
788 HOL-ZF: HOL $(LOG)/HOL-ZF.gz |
789 |
789 |
790 $(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML ZF/LProd.thy \ |
790 $(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML ZF/LProd.thy \ |
791 ZF/HOLZF.thy ZF/MainZF.thy ZF/Games.thy ZF/document/root.tex |
791 ZF/HOLZF.thy ZF/MainZF.thy ZF/Games.thy ZF/document/root.tex |
792 @$(ISABELLE_TOOL) usedir $(OUT)/HOL ZF |
792 @$(ISABELLE_TOOL) usedir $(OUT)/HOL ZF |
793 |
793 |
794 |
794 |
795 ## HOL-Imperative_HOL |
795 ## HOL-Imperative_HOL |
796 |
796 |
797 HOL-Imperative_HOL: HOL $(LOG)/HOL-Imperative_HOL.gz |
797 HOL-Imperative_HOL: HOL $(LOG)/HOL-Imperative_HOL.gz |
798 |
798 |
799 $(LOG)/HOL-Imperative_HOL.gz: $(OUT)/HOL Imperative_HOL/Array.thy \ |
799 $(LOG)/HOL-Imperative_HOL.gz: $(OUT)/HOL \ |
800 Imperative_HOL/Heap.thy Imperative_HOL/Heap_Monad.thy \ |
800 Imperative_HOL/Array.thy \ |
801 Imperative_HOL/Imperative_HOL.thy Imperative_HOL/Imperative_HOL_ex.thy\ |
801 Imperative_HOL/Heap.thy \ |
802 Imperative_HOL/Mrec.thy Imperative_HOL/Ref.thy \ |
802 Imperative_HOL/Heap_Monad.thy \ |
803 Imperative_HOL/ex/Imperative_Quicksort.thy \ |
803 Imperative_HOL/Imperative_HOL.thy \ |
804 Imperative_HOL/ex/Imperative_Reverse.thy \ |
804 Imperative_HOL/Imperative_HOL_ex.thy \ |
805 Imperative_HOL/ex/Linked_Lists.thy \ |
805 Imperative_HOL/Mrec.thy \ |
806 Imperative_HOL/ex/SatChecker.thy \ |
806 Imperative_HOL/Ref.thy \ |
807 Imperative_HOL/ex/Sorted_List.thy \ |
807 Imperative_HOL/ROOT.ML \ |
808 Imperative_HOL/ex/Subarray.thy \ |
808 Imperative_HOL/ex/Imperative_Quicksort.thy \ |
|
809 Imperative_HOL/ex/Imperative_Reverse.thy \ |
|
810 Imperative_HOL/ex/Linked_Lists.thy \ |
|
811 Imperative_HOL/ex/SatChecker.thy \ |
|
812 Imperative_HOL/ex/Sorted_List.thy \ |
|
813 Imperative_HOL/ex/Subarray.thy \ |
809 Imperative_HOL/ex/Sublist.thy |
814 Imperative_HOL/ex/Sublist.thy |
810 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Imperative_HOL |
815 @$(ISABELLE_TOOL) usedir -g true -m iff -m no_brackets $(OUT)/HOL Imperative_HOL |
811 |
816 |
812 |
817 |
813 ## HOL-Decision_Procs |
818 ## HOL-Decision_Procs |
814 |
819 |
815 HOL-Decision_Procs: HOL $(LOG)/HOL-Decision_Procs.gz |
820 HOL-Decision_Procs: HOL $(LOG)/HOL-Decision_Procs.gz |