src/HOL/Mirabelle/Mirabelle.thy
changeset 41358 d5e91925916e
parent 39155 3e94ebe282f1
child 42071 04577a7e0c51
     1.1 --- a/src/HOL/Mirabelle/Mirabelle.thy	Tue Dec 21 10:18:56 2010 +0100
     1.2 +++ b/src/HOL/Mirabelle/Mirabelle.thy	Tue Dec 21 10:24:56 2010 +0100
     1.3 @@ -3,8 +3,9 @@
     1.4  *)
     1.5  
     1.6  theory Mirabelle
     1.7 -imports Pure
     1.8 +imports Sledgehammer
     1.9  uses "Tools/mirabelle.ML"
    1.10 +     "Tools/sledgehammer_tactics.ML"
    1.11  begin
    1.12  
    1.13  (* no multithreading, no parallel proofs *)  (* FIXME *)