src/HOL/Mirabelle/Mirabelle.thy
author blanchet
Tue Dec 21 10:24:56 2010 +0100 (2010-12-21)
changeset 41358 d5e91925916e
parent 39155 3e94ebe282f1
child 42071 04577a7e0c51
permissions -rw-r--r--
renamed "sledgehammer_tactic.ML" to "sledgehammer_tactics.ML" (cf. module name);
use it in "Mirabelle.thy"
     1 (*  Title:      HOL/Mirabelle/Mirabelle.thy
     2     Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
     3 *)
     4 
     5 theory Mirabelle
     6 imports Sledgehammer
     7 uses "Tools/mirabelle.ML"
     8      "Tools/sledgehammer_tactics.ML"
     9 begin
    10 
    11 (* no multithreading, no parallel proofs *)  (* FIXME *)
    12 ML {* Multithreading.max_threads := 1 *}
    13 ML {* Goal.parallel_proofs := 0 *}
    14 
    15 ML {* Toplevel.add_hook Mirabelle.step_hook *}
    16 
    17 setup Mirabelle.setup
    18 
    19 ML {*
    20 signature MIRABELLE_ACTION =
    21 sig
    22   val invoke : (string * string) list -> theory -> theory
    23 end
    24 *}
    25 
    26 end