| author | blanchet |
| Wed, 23 Mar 2011 10:06:27 +0100 | |
| changeset 42942 | 04577a7e0c51 |
| parent 41606 | d5e91925916e |
| child 43487 | 92715b528e78 |
| permissions | -rw-r--r-- |
1 (* Title: HOL/Mirabelle/Mirabelle.thy
2 Author: Jasmin Blanchette and Sascha Boehme, TU Munich
3 *)
5 theory Mirabelle
6 imports Sledgehammer
7 uses "Tools/mirabelle.ML"
8 "../ex/sledgehammer_tactics.ML"
9 begin
11 (* no multithreading, no parallel proofs *) (* FIXME *)
12 ML {* Multithreading.max_threads := 1 *}
13 ML {* Goal.parallel_proofs := 0 *}
15 ML {* Toplevel.add_hook Mirabelle.step_hook *}
17 setup Mirabelle.setup
19 ML {*
20 signature MIRABELLE_ACTION =
21 sig
22 val invoke : (string * string) list -> theory -> theory
23 end
24 *}
26 end