647 HOL-Imperative_HOL: HOL $(LOG)/HOL-Imperative_HOL.gz |
647 HOL-Imperative_HOL: HOL $(LOG)/HOL-Imperative_HOL.gz |
648 |
648 |
649 $(LOG)/HOL-Imperative_HOL.gz: $(OUT)/HOL Imperative_HOL/Heap.thy \ |
649 $(LOG)/HOL-Imperative_HOL.gz: $(OUT)/HOL Imperative_HOL/Heap.thy \ |
650 Imperative_HOL/Heap_Monad.thy Imperative_HOL/Array.thy \ |
650 Imperative_HOL/Heap_Monad.thy Imperative_HOL/Array.thy \ |
651 Imperative_HOL/Relational.thy \ |
651 Imperative_HOL/Relational.thy \ |
652 Imperative_HOL/Ref.thy Imperative_HOL/Imperative_HOL.thy |
652 Imperative_HOL/Ref.thy Imperative_HOL/Imperative_HOL.thy \ |
|
653 Imperative_HOL/Imperative_HOL_ex.thy \ |
|
654 Imperative_HOL/ex/Imperative_Quicksort.thy \ |
|
655 Imperative_HOL/ex/Subarray.thy \ |
|
656 Imperative_HOL/ex/Sublist.thy |
653 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Imperative_HOL |
657 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Imperative_HOL |
654 |
658 |
655 |
659 |
656 ## HOL-SizeChange |
660 ## HOL-SizeChange |
657 |
661 |
834 ex/Efficient_Nat_examples.thy \ |
838 ex/Efficient_Nat_examples.thy \ |
835 ex/Eval_Examples.thy ex/ExecutableContent.thy \ |
839 ex/Eval_Examples.thy ex/ExecutableContent.thy \ |
836 ex/Formal_Power_Series_Examples.thy ex/Fundefs.thy \ |
840 ex/Formal_Power_Series_Examples.thy ex/Fundefs.thy \ |
837 ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy \ |
841 ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy \ |
838 ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy \ |
842 ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy \ |
839 ex/Hilbert_Classical.thy ex/ImperativeQuicksort.thy \ |
843 ex/Hilbert_Classical.thy \ |
840 ex/Induction_Scheme.thy ex/InductiveInvariant.thy \ |
844 ex/Induction_Scheme.thy ex/InductiveInvariant.thy \ |
841 ex/InductiveInvariant_examples.thy ex/Intuitionistic.thy \ |
845 ex/InductiveInvariant_examples.thy ex/Intuitionistic.thy \ |
842 ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy \ |
846 ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy \ |
843 ex/Meson_Test.thy ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy \ |
847 ex/Meson_Test.thy ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy \ |
844 ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \ |
848 ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \ |
845 ex/Quickcheck_Examples.thy ex/Quickcheck_Generators.thy ex/ROOT.ML \ |
849 ex/Quickcheck_Examples.thy ex/Quickcheck_Generators.thy ex/ROOT.ML \ |
846 ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy \ |
850 ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy \ |
847 ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \ |
851 ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \ |
848 ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Subarray.thy \ |
852 ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy \ |
849 ex/Sublist.thy ex/Sudoku.thy ex/Tarski.thy ex/Term_Of_Syntax.thy \ |
853 ex/Sudoku.thy ex/Tarski.thy ex/Term_Of_Syntax.thy \ |
850 ex/Termination.thy ex/Unification.thy ex/document/root.bib \ |
854 ex/Termination.thy ex/Unification.thy ex/document/root.bib \ |
851 ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy \ |
855 ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy \ |
852 ex/Predicate_Compile.thy ex/predicate_compile.ML |
856 ex/Predicate_Compile.thy ex/predicate_compile.ML |
853 @$(ISABELLE_TOOL) usedir $(OUT)/HOL ex |
857 @$(ISABELLE_TOOL) usedir $(OUT)/HOL ex |
854 |
858 |