equal
deleted
inserted
replaced
834 ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy \ |
834 ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy \ |
835 ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \ |
835 ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \ |
836 ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Subarray.thy \ |
836 ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Subarray.thy \ |
837 ex/Sublist.thy ex/Sudoku.thy ex/Tarski.thy ex/Term_Of_Syntax.thy \ |
837 ex/Sublist.thy ex/Sudoku.thy ex/Tarski.thy ex/Term_Of_Syntax.thy \ |
838 ex/Termination.thy ex/Unification.thy ex/document/root.bib \ |
838 ex/Termination.thy ex/Unification.thy ex/document/root.bib \ |
839 ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy |
839 ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy \ |
|
840 ex/Predicate_Compile.thy ex/predicate_compile.ML |
840 @$(ISABELLE_TOOL) usedir $(OUT)/HOL ex |
841 @$(ISABELLE_TOOL) usedir $(OUT)/HOL ex |
841 |
842 |
842 |
843 |
843 ## HOL-Isar_examples |
844 ## HOL-Isar_examples |
844 |
845 |