equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 theory Mirabelle |
5 theory Mirabelle |
6 imports Sledgehammer |
6 imports Sledgehammer |
7 uses "Tools/mirabelle.ML" |
7 uses "Tools/mirabelle.ML" |
8 "../ex/sledgehammer_tactics.ML" |
8 "../TPTP/sledgehammer_tactics.ML" |
9 begin |
9 begin |
10 |
10 |
11 (* no multithreading, no parallel proofs *) (* FIXME *) |
11 (* no multithreading, no parallel proofs *) (* FIXME *) |
12 ML {* Multithreading.max_threads := 1 *} |
12 ML {* Multithreading.max_threads := 1 *} |
13 ML {* Goal.parallel_proofs := 0 *} |
13 ML {* Goal.parallel_proofs := 0 *} |