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