author | sultana |
Tue, 24 Apr 2012 13:59:29 +0100 | |
changeset 47730 | 15f4309bb9eb |
parent 47477 | 3fabf352243e |
child 47790 | 2e1636e45770 |
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