1.1 --- a/src/HOL/Tools/Mirabelle/Mirabelle.thy	Fri Aug 21 09:49:10 2009 +0200
     1.2 +++ b/src/HOL/Tools/Mirabelle/Mirabelle.thy	Fri Aug 21 13:21:19 2009 +0200
     1.3 @@ -3,10 +3,23 @@
     1.4  *)
     1.5  
     1.6  theory Mirabelle
     1.7 -imports Plain
     1.8 +imports Pure
     1.9  uses "Tools/mirabelle.ML"
    1.10  begin
    1.11  
    1.12 +(* no multithreading, no parallel proofs *)
    1.13 +ML {* Multithreading.max_threads := 1 *}
    1.14 +ML {* Goal.parallel_proofs := 0 *}
    1.15 +
    1.16 +ML {* Toplevel.add_hook Mirabelle.step_hook *}
    1.17 +
    1.18  setup Mirabelle.setup
    1.19  
    1.20 +ML {*
    1.21 +signature MIRABELLE_ACTION =
    1.22 +sig
    1.23 +  val invoke : (string * string) list -> theory -> theory
    1.24  end
    1.25 +*}
    1.26 +
    1.27 +end