author | blanchet |
Fri, 27 May 2011 10:30:08 +0200 | |
changeset 43016 | 42330f25142c |
parent 42616 | 92715b528e78 |
child 47477 | 3fabf352243e |
permissions | -rw-r--r-- |
32564 | 1 |
(* Title: HOL/Mirabelle/Mirabelle.thy |
2 |
Author: Jasmin Blanchette and Sascha Boehme, TU Munich |
|
32381 | 3 |
*) |
4 |
||
5 |
theory Mirabelle |
|
41358
d5e91925916e
renamed "sledgehammer_tactic.ML" to "sledgehammer_tactics.ML" (cf. module name);
blanchet
parents:
39155
diff
changeset
|
6 |
imports Sledgehammer |
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
7 |
uses "Tools/mirabelle.ML" |
42071
04577a7e0c51
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents:
41358
diff
changeset
|
8 |
"../ex/sledgehammer_tactics.ML" |
32381 | 9 |
begin |
10 |
||
39155 | 11 |
(* no multithreading, no parallel proofs *) (* FIXME *) |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
12 |
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
|
13 |
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
|
14 |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
15 |
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
|
16 |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
17 |
ML {* |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
18 |
signature MIRABELLE_ACTION = |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
19 |
sig |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
20 |
val invoke : (string * string) list -> theory -> theory |
32381 | 21 |
end |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
22 |
*} |
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 |
end |