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-- |
32381 | 1 |
(* Title: Mirabelle.thy |
2 |
Author: Jasmin Blanchette and Sascha Boehme |
|
3 |
*) |
|
4 |
||
5 |
theory Mirabelle |
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
6 |
imports Pure |
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
7 |
uses "Tools/mirabelle.ML" |
32381 | 8 |
begin |
9 |
||
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
10 |
(* no multithreading, no parallel proofs *) |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
11 |
ML {* Multithreading.max_threads := 1 *} |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
12 |
ML {* Goal.parallel_proofs := 0 *} |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
13 |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
14 |
ML {* Toplevel.add_hook Mirabelle.step_hook *} |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
15 |
|
32381 | 16 |
setup Mirabelle.setup |
17 |
||
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
18 |
ML {* |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
19 |
signature MIRABELLE_ACTION = |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
20 |
sig |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
21 |
val invoke : (string * string) list -> theory -> theory |
32381 | 22 |
end |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
23 |
*} |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
24 |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
25 |
end |