src/HOL/Mirabelle/Mirabelle.thy
author boehmes
Wed Sep 02 16:23:53 2009 +0200 (2009-09-02)
changeset 32496 4ab00a2642c3
parent 32385 src/HOL/Tools/Mirabelle/Mirabelle.thy@594890623c46
child 32564 378528d2f7eb
permissions -rw-r--r--
moved Mirabelle from HOL/Tools to HOL,
added session HOL-Mirabelle
     1 (* Title: Mirabelle.thy
     2    Author: Jasmin Blanchette and Sascha Boehme
     3 *)
     4 
     5 theory Mirabelle
     6 imports Pure
     7 uses "Tools/mirabelle.ML"
     8 begin
     9 
    10 (* no multithreading, no parallel proofs *)
    11 ML {* Multithreading.max_threads := 1 *}
    12 ML {* Goal.parallel_proofs := 0 *}
    13 
    14 ML {* Toplevel.add_hook Mirabelle.step_hook *}
    15 
    16 setup Mirabelle.setup
    17 
    18 ML {*
    19 signature MIRABELLE_ACTION =
    20 sig
    21   val invoke : (string * string) list -> theory -> theory
    22 end
    23 *}
    24 
    25 end