changeset 48891 | c0eafbd55de3 |
parent 47790 | 2e1636e45770 |
child 49550 | 0a82e98fd4a3 |
--- a/src/HOL/Mirabelle/Mirabelle.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Mirabelle/Mirabelle.thy Wed Aug 22 22:55:41 2012 +0200 @@ -4,10 +4,11 @@ theory Mirabelle imports Sledgehammer -uses "Tools/mirabelle.ML" - "../TPTP/sledgehammer_tactics.ML" begin +ML_file "Tools/mirabelle.ML" +ML_file "../TPTP/sledgehammer_tactics.ML" + (* no multithreading, no parallel proofs *) (* FIXME *) ML {* Multithreading.max_threads := 1 *} ML {* Goal.parallel_proofs := 0 *}