changeset 41358 | d5e91925916e |
parent 39155 | 3e94ebe282f1 |
child 42071 | 04577a7e0c51 |
--- a/src/HOL/Mirabelle/Mirabelle.thy Tue Dec 21 10:18:56 2010 +0100 +++ b/src/HOL/Mirabelle/Mirabelle.thy Tue Dec 21 10:24:56 2010 +0100 @@ -3,8 +3,9 @@ *) theory Mirabelle -imports Pure +imports Sledgehammer uses "Tools/mirabelle.ML" + "Tools/sledgehammer_tactics.ML" begin (* no multithreading, no parallel proofs *) (* FIXME *)