author | wenzelm |
Sat, 14 Jan 2012 12:36:43 +0100 | |
changeset 46204 | df1369a42393 |
parent 42616 | 92715b528e78 |
child 47477 | 3fabf352243e |
permissions | -rw-r--r-- |
(* Title: HOL/Mirabelle/Mirabelle.thy Author: Jasmin Blanchette and Sascha Boehme, TU Munich *) theory Mirabelle imports Sledgehammer uses "Tools/mirabelle.ML" "../ex/sledgehammer_tactics.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 *} ML {* signature MIRABELLE_ACTION = sig val invoke : (string * string) list -> theory -> theory end *} end