equal
deleted
inserted
replaced
1 (* Title: Mirabelle.thy |
1 (* Title: Mirabelle.thy |
2 Author: Jasmin Blanchette and Sascha Boehme |
2 Author: Jasmin Blanchette and Sascha Boehme |
3 *) |
3 *) |
4 |
4 |
5 theory Mirabelle |
5 theory Mirabelle |
6 imports Plain |
6 imports Pure |
7 uses "Tools/mirabelle.ML" |
7 uses "Tools/mirabelle.ML" |
8 begin |
8 begin |
9 |
9 |
|
10 (* no multithreading, no parallel proofs *) |
|
11 ML {* Multithreading.max_threads := 1 *} |
|
12 ML {* Goal.parallel_proofs := 0 *} |
|
13 |
|
14 ML {* Toplevel.add_hook Mirabelle.step_hook *} |
|
15 |
10 setup Mirabelle.setup |
16 setup Mirabelle.setup |
11 |
17 |
|
18 ML {* |
|
19 signature MIRABELLE_ACTION = |
|
20 sig |
|
21 val invoke : (string * string) list -> theory -> theory |
12 end |
22 end |
|
23 *} |
|
24 |
|
25 end |