| author | boehmes |
| Wed, 02 Sep 2009 16:23:53 +0200 | |
| changeset 32496 | 4ab00a2642c3 |
| parent 32385 | src/HOL/Tools/Mirabelle/Mirabelle.thy@594890623c46 |
| child 32564 | 378528d2f7eb |
| permissions | -rw-r--r-- |
1 (* Title: Mirabelle.thy
2 Author: Jasmin Blanchette and Sascha Boehme
3 *)
5 theory Mirabelle
6 imports Pure
7 uses "Tools/mirabelle.ML"
8 begin
10 (* no multithreading, no parallel proofs *)
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