src/HOL/Mirabelle/Mirabelle.thy
changeset 49550 0a82e98fd4a3
parent 48891 c0eafbd55de3
child 59574 de392405a851
equal deleted inserted replaced
49549:3b0a60eee56e 49550:0a82e98fd4a3
     7 begin
     7 begin
     8 
     8 
     9 ML_file "Tools/mirabelle.ML"
     9 ML_file "Tools/mirabelle.ML"
    10 ML_file "../TPTP/sledgehammer_tactics.ML"
    10 ML_file "../TPTP/sledgehammer_tactics.ML"
    11 
    11 
    12 (* no multithreading, no parallel proofs *)  (* FIXME *)
       
    13 ML {* Multithreading.max_threads := 1 *}
       
    14 ML {* Goal.parallel_proofs := 0 *}
       
    15 
       
    16 ML {* Toplevel.add_hook Mirabelle.step_hook *}
    12 ML {* Toplevel.add_hook Mirabelle.step_hook *}
    17 
    13 
    18 ML {*
    14 ML {*
    19 signature MIRABELLE_ACTION =
    15 signature MIRABELLE_ACTION =
    20 sig
    16 sig