equal
deleted
inserted
replaced
1032 ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \ |
1032 ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \ |
1033 ex/Quicksort.thy ex/ROOT.ML \ |
1033 ex/Quicksort.thy ex/ROOT.ML \ |
1034 ex/Records.thy ex/ReflectionEx.thy ex/Refute_Examples.thy \ |
1034 ex/Records.thy ex/ReflectionEx.thy ex/Refute_Examples.thy \ |
1035 ex/SAT_Examples.thy ex/Serbian.thy ex/Set_Theory.thy \ |
1035 ex/SAT_Examples.thy ex/Serbian.thy ex/Set_Theory.thy \ |
1036 ex/Simproc_Tests.thy ex/SVC_Oracle.thy \ |
1036 ex/Simproc_Tests.thy ex/SVC_Oracle.thy \ |
1037 ex/sledgehammer_tactics.ML ex/Seq.thy ex/Sqrt.thy ex/Sqrt_Script.thy \ |
1037 ex/Seq.thy ex/Sqrt.thy ex/Sqrt_Script.thy \ |
1038 ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy \ |
1038 ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy \ |
1039 ex/Transfer_Int_Nat.thy \ |
1039 ex/Transfer_Int_Nat.thy \ |
1040 ex/Tree23.thy ex/Unification.thy ex/While_Combinator_Example.thy \ |
1040 ex/Tree23.thy ex/Unification.thy ex/While_Combinator_Example.thy \ |
1041 ex/document/root.bib ex/document/root.tex ex/svc_funcs.ML \ |
1041 ex/document/root.bib ex/document/root.tex ex/svc_funcs.ML \ |
1042 ex/svc_test.thy ../Tools/interpretation_with_defs.ML |
1042 ex/svc_test.thy ../Tools/interpretation_with_defs.ML |
1151 TPTP/TPTP_Parser/tptp_parser.ML \ |
1151 TPTP/TPTP_Parser/tptp_parser.ML \ |
1152 TPTP/TPTP_Parser/tptp_problem_name.ML \ |
1152 TPTP/TPTP_Parser/tptp_problem_name.ML \ |
1153 TPTP/TPTP_Parser/tptp_syntax.ML \ |
1153 TPTP/TPTP_Parser/tptp_syntax.ML \ |
1154 TPTP/TPTP_Parser_Test.thy \ |
1154 TPTP/TPTP_Parser_Test.thy \ |
1155 TPTP/atp_problem_import.ML \ |
1155 TPTP/atp_problem_import.ML \ |
1156 TPTP/atp_theory_export.ML |
1156 TPTP/atp_theory_export.ML \ |
|
1157 TPTP/sledgehammer_tactics.ML |
1157 @$(ISABELLE_TOOL) usedir $(OUT)/HOL TPTP |
1158 @$(ISABELLE_TOOL) usedir $(OUT)/HOL TPTP |
1158 |
1159 |
1159 |
1160 |
1160 ## HOL-Multivariate_Analysis |
1161 ## HOL-Multivariate_Analysis |
1161 |
1162 |
1331 Mirabelle/Tools/mirabelle_metis.ML \ |
1332 Mirabelle/Tools/mirabelle_metis.ML \ |
1332 Mirabelle/Tools/mirabelle_quickcheck.ML \ |
1333 Mirabelle/Tools/mirabelle_quickcheck.ML \ |
1333 Mirabelle/Tools/mirabelle_refute.ML \ |
1334 Mirabelle/Tools/mirabelle_refute.ML \ |
1334 Mirabelle/Tools/mirabelle_sledgehammer.ML \ |
1335 Mirabelle/Tools/mirabelle_sledgehammer.ML \ |
1335 Mirabelle/Tools/mirabelle_sledgehammer_filter.ML \ |
1336 Mirabelle/Tools/mirabelle_sledgehammer_filter.ML \ |
1336 ex/sledgehammer_tactics.ML Mirabelle/lib/Tools/mirabelle \ |
1337 TPTP/sledgehammer_tactics.ML Mirabelle/lib/Tools/mirabelle \ |
1337 Mirabelle/lib/scripts/mirabelle.pl Library/FrechetDeriv.thy \ |
1338 Mirabelle/lib/scripts/mirabelle.pl Library/FrechetDeriv.thy \ |
1338 Library/Inner_Product.thy |
1339 Library/Inner_Product.thy |
1339 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle |
1340 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle |
1340 @cd Library; $(ISABELLE_TOOL) mirabelle -q arith Inner_Product.thy # some arbitrary small test case |
1341 @cd Library; $(ISABELLE_TOOL) mirabelle -q arith Inner_Product.thy # some arbitrary small test case |
1341 |
1342 |