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