changeset 42071 | 04577a7e0c51 |
parent 41358 | d5e91925916e |
child 42616 | 92715b528e78 |
--- a/src/HOL/Mirabelle/Mirabelle.thy Wed Mar 23 09:15:49 2011 +0100 +++ b/src/HOL/Mirabelle/Mirabelle.thy Wed Mar 23 10:06:27 2011 +0100 @@ -5,7 +5,7 @@ theory Mirabelle imports Sledgehammer uses "Tools/mirabelle.ML" - "Tools/sledgehammer_tactics.ML" + "../ex/sledgehammer_tactics.ML" begin (* no multithreading, no parallel proofs *) (* FIXME *)