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