| author | boehmes |
| Fri, 21 Aug 2009 13:21:19 +0200 | |
| changeset 32385 | 594890623c46 |
| parent 32383 | 521065a499c6 |
| 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