src/HOL/Tools/Mirabelle/Mirabelle.thy
changeset 32496 4ab00a2642c3
parent 32495 6decc1ffdbed
child 32497 922718ac81e4
--- a/src/HOL/Tools/Mirabelle/Mirabelle.thy	Wed Sep 02 16:02:37 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-(* 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