src/HOL/Mirabelle/Mirabelle.thy
changeset 42616 92715b528e78
parent 42071 04577a7e0c51
child 47477 3fabf352243e
equal deleted inserted replaced
42607:c8673078f915 42616:92715b528e78
    12 ML {* Multithreading.max_threads := 1 *}
    12 ML {* Multithreading.max_threads := 1 *}
    13 ML {* Goal.parallel_proofs := 0 *}
    13 ML {* Goal.parallel_proofs := 0 *}
    14 
    14 
    15 ML {* Toplevel.add_hook Mirabelle.step_hook *}
    15 ML {* Toplevel.add_hook Mirabelle.step_hook *}
    16 
    16 
    17 setup Mirabelle.setup
       
    18 
       
    19 ML {*
    17 ML {*
    20 signature MIRABELLE_ACTION =
    18 signature MIRABELLE_ACTION =
    21 sig
    19 sig
    22   val invoke : (string * string) list -> theory -> theory
    20   val invoke : (string * string) list -> theory -> theory
    23 end
    21 end