--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/Mirabelle.thy Wed Sep 02 16:23:53 2009 +0200
@@ -0,0 +1,25 @@
+(* Title: Mirabelle.thy
+ Author: Jasmin Blanchette and Sascha Boehme
+*)
+
+theory Mirabelle
+imports Pure
+uses "Tools/mirabelle.ML"
+begin
+
+(* no multithreading, no parallel proofs *)
+ML {* Multithreading.max_threads := 1 *}
+ML {* Goal.parallel_proofs := 0 *}
+
+ML {* Toplevel.add_hook Mirabelle.step_hook *}
+
+setup Mirabelle.setup
+
+ML {*
+signature MIRABELLE_ACTION =
+sig
+ val invoke : (string * string) list -> theory -> theory
+end
+*}
+
+end