author | wenzelm |
Wed, 22 Aug 2012 22:55:41 +0200 | |
changeset 48891 | c0eafbd55de3 |
parent 47790 | 2e1636e45770 |
child 49550 | 0a82e98fd4a3 |
permissions | -rw-r--r-- |
(* Title: HOL/Mirabelle/Mirabelle.thy Author: Jasmin Blanchette and Sascha Boehme, TU Munich *) theory Mirabelle imports Sledgehammer begin ML_file "Tools/mirabelle.ML" ML_file "../TPTP/sledgehammer_tactics.ML" (* 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