equal
deleted
inserted
replaced
7 begin |
7 begin |
8 |
8 |
9 ML_file "Tools/mirabelle.ML" |
9 ML_file "Tools/mirabelle.ML" |
10 ML_file "../TPTP/sledgehammer_tactics.ML" |
10 ML_file "../TPTP/sledgehammer_tactics.ML" |
11 |
11 |
12 (* no multithreading, no parallel proofs *) (* FIXME *) |
|
13 ML {* Multithreading.max_threads := 1 *} |
|
14 ML {* Goal.parallel_proofs := 0 *} |
|
15 |
|
16 ML {* Toplevel.add_hook Mirabelle.step_hook *} |
12 ML {* Toplevel.add_hook Mirabelle.step_hook *} |
17 |
13 |
18 ML {* |
14 ML {* |
19 signature MIRABELLE_ACTION = |
15 signature MIRABELLE_ACTION = |
20 sig |
16 sig |