changeset 47790 | 2e1636e45770 |
parent 47730 | 15f4309bb9eb |
child 48891 | c0eafbd55de3 |
--- a/src/HOL/Mirabelle/Mirabelle.thy Fri Apr 27 14:07:31 2012 +0200 +++ b/src/HOL/Mirabelle/Mirabelle.thy Fri Apr 27 15:24:37 2012 +0200 @@ -5,7 +5,7 @@ theory Mirabelle imports Sledgehammer uses "Tools/mirabelle.ML" - "../ex/sledgehammer_tactics.ML" + "../TPTP/sledgehammer_tactics.ML" begin (* no multithreading, no parallel proofs *) (* FIXME *)