| author | wenzelm |
| Mon, 06 Sep 2010 13:06:27 +0200 | |
| changeset 39402 | 3e94ebe282f1 |
| parent 32564 | 378528d2f7eb |
| child 41606 | d5e91925916e |
| 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 Pure
7 uses "Tools/mirabelle.ML"
8 begin
10 (* no multithreading, no parallel proofs *) (* FIXME *)
11 ML {* Multithreading.max_threads := 1 *}
12 ML {* Goal.parallel_proofs := 0 *}
14 ML {* Toplevel.add_hook Mirabelle.step_hook *}
16 setup Mirabelle.setup
18 ML {*
19 signature MIRABELLE_ACTION =
20 sig
21 val invoke : (string * string) list -> theory -> theory
22 end
23 *}
25 end