# HG changeset patch
# User blanchet
# Date 1336386055 -7200
# Node ID e3627a83b1141fbc2fc46c970be7217cc5f121d1
# Parent  0cedab5d2eb7c9e607756c28e26d7a1a1dfe2ce0
added "try0" tool to Mirabelle

diff -r 0cedab5d2eb7 -r e3627a83b114 src/HOL/Mirabelle/Mirabelle_Test.thy
--- a/src/HOL/Mirabelle/Mirabelle_Test.thy	Mon May 07 12:20:55 2012 +0200
+++ b/src/HOL/Mirabelle/Mirabelle_Test.thy	Mon May 07 12:20:55 2012 +0200
@@ -13,6 +13,7 @@
   "Tools/mirabelle_refute.ML"
   "Tools/mirabelle_sledgehammer.ML"
   "Tools/mirabelle_sledgehammer_filter.ML"
+  "Tools/mirabelle_try0.ML"
 begin
 
 text {*
diff -r 0cedab5d2eb7 -r e3627a83b114 src/HOL/Mirabelle/Tools/mirabelle_try0.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/Tools/mirabelle_try0.ML	Mon May 07 12:20:55 2012 +0200
@@ -0,0 +1,21 @@
+(*  Title:      HOL/Mirabelle/Actions/mirabelle_try0.ML
+    Author:     Jasmin Blanchette, TU Munich
+*)
+
+structure Mirabelle_Try0 : MIRABELLE_ACTION =
+struct
+
+fun try0_tag id = "#" ^ string_of_int id ^ " try0: "
+
+fun init _ = I
+fun done _ _ = ()
+
+fun run id ({pre, (* timeout, *) log, ...}: Mirabelle.run_args) =
+  if Try0.try0 (* (SOME timeout) *) NONE ([], [], [], []) pre
+  then log (try0_tag id ^ "succeeded")
+  else ()
+  handle TimeLimit.TimeOut => log (try0_tag id ^ "timeout")
+
+fun invoke _ = Mirabelle.register (init, Mirabelle.catch try0_tag run, done)
+
+end