author | wenzelm |
Mon, 06 Sep 2010 13:06:27 +0200 | |
changeset 39155 | 3e94ebe282f1 |
parent 32564 | 378528d2f7eb |
child 41358 | d5e91925916e |
permissions | -rw-r--r-- |
(* Title: HOL/Mirabelle/Mirabelle.thy Author: Jasmin Blanchette and Sascha Boehme, TU Munich *) theory Mirabelle imports Pure uses "Tools/mirabelle.ML" begin (* no multithreading, no parallel proofs *) (* FIXME *) ML {* Multithreading.max_threads := 1 *} ML {* Goal.parallel_proofs := 0 *} ML {* Toplevel.add_hook Mirabelle.step_hook *} setup Mirabelle.setup ML {* signature MIRABELLE_ACTION = sig val invoke : (string * string) list -> theory -> theory end *} end