src/HOL/Mirabelle/Mirabelle.thy
changeset 32496 4ab00a2642c3
parent 32385 594890623c46
child 32564 378528d2f7eb
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Mirabelle/Mirabelle.thy	Wed Sep 02 16:23:53 2009 +0200
     1.3 @@ -0,0 +1,25 @@
     1.4 +(* Title: Mirabelle.thy
     1.5 +   Author: Jasmin Blanchette and Sascha Boehme
     1.6 +*)
     1.7 +
     1.8 +theory Mirabelle
     1.9 +imports Pure
    1.10 +uses "Tools/mirabelle.ML"
    1.11 +begin
    1.12 +
    1.13 +(* no multithreading, no parallel proofs *)
    1.14 +ML {* Multithreading.max_threads := 1 *}
    1.15 +ML {* Goal.parallel_proofs := 0 *}
    1.16 +
    1.17 +ML {* Toplevel.add_hook Mirabelle.step_hook *}
    1.18 +
    1.19 +setup Mirabelle.setup
    1.20 +
    1.21 +ML {*
    1.22 +signature MIRABELLE_ACTION =
    1.23 +sig
    1.24 +  val invoke : (string * string) list -> theory -> theory
    1.25 +end
    1.26 +*}
    1.27 +
    1.28 +end