added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods

--- a/etc/isar-keywords.el	Fri May 27 10:30:08 2011 +0200
+++ b/etc/isar-keywords.el	Fri May 27 10:30:08 2011 +0200
@@ -253,6 +253,7 @@
     "thy_deps"
     "translations"
     "try"
+    "try_methods"
     "txt"
     "txt_raw"
     "typ"
@@ -411,6 +412,7 @@
     "thm_deps"
     "thy_deps"
     "try"
+    "try_methods"
     "typ"
     "unused_thms"
     "value"

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri May 27 10:30:08 2011 +0200
@@ -582,7 +582,8 @@
         Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)
       val minimize = AList.defined (op =) args minimizeK
       val metis_ft = AList.defined (op =) args metis_ftK
-      val trivial = Try.invoke_try (SOME try_timeout) ([], [], [], []) pre
+      val trivial =
+        Try_Methods.try_methods (SOME try_timeout) ([], [], [], []) pre
         handle TimeLimit.TimeOut => false
       fun apply_reconstructor m1 m2 =
         if metis_ft

--- a/src/HOL/Tools/Nitpick/nitpick.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Fri May 27 10:30:08 2011 +0200
@@ -55,6 +55,11 @@
      batch_size: int,
      expect: string}
 
+  val genuineN : string
+  val quasi_genuineN : string
+  val potentialN : string
+  val noneN : string
+  val unknownN : string
   val register_frac_type : string -> (string * string) list -> theory -> theory
   val unregister_frac_type : string -> theory -> theory
   val register_codatatype : typ -> string -> styp list -> theory -> theory
@@ -131,6 +136,12 @@
    batch_size: int,
    expect: string}
 
+val genuineN = "genuine"
+val quasi_genuineN = "quasi_genuine"
+val potentialN = "potential"
+val noneN = "none"
+val unknownN = "unknown"
+
 (* TODO: eliminate these historical aliases *)
 val register_frac_type = Nitpick_HOL.register_frac_type_global
 val unregister_frac_type = Nitpick_HOL.unregister_frac_type_global
@@ -973,7 +984,7 @@
     fun run_batches _ _ []
                     (found_really_genuine, max_potential, max_genuine, donno) =
         if donno > 0 andalso max_genuine > 0 then
-          (print_m (fn () => excipit "checked"); "unknown")
+          (print_m (fn () => excipit "checked"); unknownN)
         else if max_genuine = original_max_genuine then
           if max_potential = original_max_potential then
             (print_m (fn () =>
@@ -982,7 +993,7 @@
                     " This suggests that the induction hypothesis might be \
                     \general enough to prove this subgoal."
                   else
-                    "")); if skipped > 0 then "unknown" else "none")
+                    "")); if skipped > 0 then unknownN else noneN)
           else
             (print_m (fn () =>
                  excipit ("could not find a" ^
@@ -991,11 +1002,11 @@
                            else
                              "ny better " ^ das_wort_model ^ "s.") ^
                           " It checked"));
-             "potential")
+             potentialN)
         else if found_really_genuine then
-          "genuine"
+          genuineN
         else
-          "quasi_genuine"
+          quasi_genuineN
       | run_batches j n (batch :: batches) z =
         let val (z as (_, _, max_genuine, _)) = run_batch j n batch z in
           run_batches (j + 1) n (if max_genuine > 0 then batches else []) z
@@ -1007,7 +1018,7 @@
                   (false, max_potential, max_genuine, 0)
       handle TimeLimit.TimeOut =>
              (print_m (fn () => excipit "ran out of time after checking");
-              if !met_potential > 0 then "potential" else "unknown")
+              if !met_potential > 0 then potentialN else unknownN)
     val _ = print_v (fn () =>
                 "Total time: " ^ string_from_time (Timer.checkRealTimer timer) ^
                 ".")
@@ -1026,7 +1037,7 @@
        ("no_kodkodi", state))
     else
       let
-        val unknown_outcome = ("unknown", state)
+        val unknown_outcome = (unknownN, state)
         val deadline = Option.map (curry Time.+ (Time.now ())) timeout
         val outcome as (outcome_code, _) =
           time_limit (if debug orelse is_none timeout then NONE
@@ -1065,7 +1076,7 @@
     val t = state |> Proof.raw_goal |> #goal |> prop_of
   in
     case Logic.count_prems t of
-      0 => (Output.urgent_message "No subgoal!"; ("none", state))
+      0 => (Output.urgent_message "No subgoal!"; (noneN, state))
     | n =>
       let
         val t = Logic.goal_params t i |> fst

--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Fri May 27 10:30:08 2011 +0200
@@ -10,6 +10,8 @@
 sig
   type params = Nitpick.params
 
+  val nitpickN : string
+  val nitpick_paramsN : string
   val auto : bool Unsynchronized.ref
   val default_params : theory -> (string * string) list -> params
   val setup : theory -> theory
@@ -24,6 +26,9 @@
 open Nitpick_Nut
 open Nitpick
 
+val nitpickN = "nitpick"
+val nitpick_paramsN = "nitpick_params"
+
 val auto = Unsynchronized.ref false
 
 (* Maximum number of scopes for Auto Nitpick. Be frugal since it has to share
@@ -356,18 +361,18 @@
     val params as {blocking, debug, ...} =
       extract_params ctxt auto (default_raw_params thy) override_params
     fun go () =
-      (false, state)
+      (unknownN, state)
       |> (if auto then perhaps o try
           else if debug then fn f => fn x => f x
           else handle_exceptions ctxt)
-         (fn (_, state) => pick_nits_in_subgoal state params auto i step
-                           |>> curry (op =) "genuine")
-  in if blocking then go () else Future.fork (tap go) |> K (false, state) end
+         (fn (_, state) => pick_nits_in_subgoal state params auto i step)
+  in if blocking then go () else Future.fork (tap go) |> K (unknownN, state) end
+  |> `(fn (outcome_code, _) => outcome_code = genuineN)
 
 fun nitpick_trans (params, i) =
-  Toplevel.keep (fn st =>
-      (pick_nits params false i (Toplevel.proof_position_of st)
-                 (Toplevel.proof_of st); ()))
+  Toplevel.keep (fn state =>
+      pick_nits params false i (Toplevel.proof_position_of state)
+                (Toplevel.proof_of state) |> K ())
 
 fun string_for_raw_param (name, value) =
   name ^ " = " ^ stringify_raw_param_value value
@@ -388,15 +393,15 @@
   (parse_params -- Scan.optional Parse.nat 1) #>> nitpick_trans
 val parse_nitpick_params_command = parse_params #>> nitpick_params_trans
 
-val _ = Outer_Syntax.improper_command "nitpick"
+val _ = Outer_Syntax.improper_command nitpickN
             "try to find a counterexample for a given subgoal using Nitpick"
             Keyword.diag parse_nitpick_command
-val _ = Outer_Syntax.command "nitpick_params"
+val _ = Outer_Syntax.command nitpick_paramsN
             "set and display the default parameters for Nitpick"
             Keyword.thy_decl parse_nitpick_params_command
 
-val auto_nitpick = pick_nits [] true 1 0
+fun try_nitpick auto = pick_nits [] auto 1 0
 
-val setup = Try.register_tool (auto, auto_nitpick)
+val setup = Try.register_tool (nitpickN, (auto, try_nitpick))
 
 end;

--- a/src/HOL/Tools/Nitpick/nitrox.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitrox.ML	Fri May 27 10:30:08 2011 +0200
@@ -124,7 +124,7 @@
          ("format", "1000"),
          ("max_potential", "0"),
          (* ("timeout", "240 s"), *)
-         ("expect", "genuine")]
+         ("expect", Nitpick.genuineN)]
         |> Nitpick_Isar.default_params @{theory}
       val auto = false
       val i = 1

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 27 10:30:08 2011 +0200
@@ -8,6 +8,7 @@
 sig
   type params = Sledgehammer_Provers.params
 
+  val sledgehammerN : string
   val auto : bool Unsynchronized.ref
   val provers : string Unsynchronized.ref
   val timeout : int Unsynchronized.ref
@@ -26,6 +27,17 @@
 open Sledgehammer_Minimize
 open Sledgehammer_Run
 
+val sledgehammerN = "sledgehammer"
+val sledgehammer_paramsN = "sledgehammer_params"
+
+val runN = "run"
+val minN = "min"
+val messagesN = "messages"
+val supported_proversN = "supported_provers"
+val running_proversN = "running_provers"
+val kill_proversN = "kill_provers"
+val refresh_tptpN = "refresh_tptp"
+
 val auto = Unsynchronized.ref false
 
 val _ =
@@ -296,17 +308,6 @@
 
 (* Sledgehammer the given subgoal *)
 
-val sledgehammerN = "sledgehammer"
-val sledgehammer_paramsN = "sledgehammer_params"
-
-val runN = "run"
-val minN = "min"
-val messagesN = "messages"
-val supported_proversN = "supported_provers"
-val running_proversN = "running_provers"
-val kill_proversN = "kill_provers"
-val refresh_tptpN = "refresh_tptp"
-
 val is_raw_param_relevant_for_minimize =
   member (op =) params_for_minimize o fst o unalias_raw_param
 fun string_for_raw_param (key, values) =
@@ -402,12 +403,15 @@
       "set and display the default parameters for Sledgehammer" Keyword.thy_decl
       parse_sledgehammer_params_command
 
-fun auto_sledgehammer state =
-  let val ctxt = Proof.context_of state in
-    run_sledgehammer (get_params true ctxt []) true 1 no_relevance_override
-                     (minimize_command [] 1) state
+fun try_sledgehammer auto state =
+  let
+    val ctxt = Proof.context_of state
+    val i = 1
+  in
+    run_sledgehammer (get_params auto ctxt []) auto i no_relevance_override
+                     (minimize_command [] i) state
   end
 
-val setup = Try.register_tool (auto, auto_sledgehammer)
+val setup = Try.register_tool (sledgehammerN, (auto, try_sledgehammer))
 
 end;

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri May 27 10:30:08 2011 +0200
@@ -13,11 +13,15 @@
   type params = Sledgehammer_Provers.params
   type prover = Sledgehammer_Provers.prover
 
+  val someN : string
+  val noneN : string
+  val timeoutN : string
+  val unknownN : string
   val auto_minimize_min_facts : int Config.T
   val get_minimizing_prover : Proof.context -> bool -> string -> prover
   val run_sledgehammer :
     params -> bool -> int -> relevance_override -> (string -> minimize_command)
-    -> Proof.state -> bool * Proof.state
+    -> Proof.state -> bool * (string * Proof.state)
 end;
 
 structure Sledgehammer_Run : SLEDGEHAMMER_RUN =
@@ -29,6 +33,22 @@
 open Sledgehammer_Provers
 open Sledgehammer_Minimize
 
+val someN = "some"
+val noneN = "none"
+val timeoutN = "timeout"
+val unknownN = "unknown"
+
+val ordered_outcome_codes = [someN, unknownN, timeoutN, noneN]
+
+fun max_outcome_code codes =
+  NONE
+  |> fold (fn candidate =>
+              fn accum as SOME _ => accum
+               | NONE => if member (op =) codes candidate then SOME candidate
+                         else NONE)
+          ordered_outcome_codes
+  |> the_default unknownN
+
 fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i
                        n goal =
   (name,
@@ -86,11 +106,6 @@
              | NONE => result
            end)
 
-val someN = "some"
-val noneN = "none"
-val timeoutN = "timeout"
-val unknownN = "unknown"
-
 fun launch_prover (params as {debug, blocking, max_relevant, slicing, timeout,
                               expect, ...})
         auto minimize_command only
@@ -190,7 +205,7 @@
   if null provers then
     error "No prover is set."
   else case subgoal_count state of
-    0 => (Output.urgent_message "No subgoal!"; (false, state))
+    0 => (Output.urgent_message "No subgoal!"; (false, (noneN, state)))
   | n =>
     let
       val _ = Proof.assert_backward state
@@ -219,18 +234,19 @@
              facts = facts,
              smt_filter = maybe_smt_filter
                   (fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i}
-          fun launch problem =
-            launch_prover params auto minimize_command only problem
-            #>> curry (op =) someN
+          val launch = launch_prover params auto minimize_command only
         in
           if auto then
-            fold (fn prover => fn (true, state) => (true, state)
-                                | (false, _) => launch problem prover)
-                 provers (false, state)
+            (unknownN, state)
+            |> fold (fn prover => fn accum as (outcome_code, state) =>
+                        if outcome_code = someN then accum
+                        else launch problem prover)
+                    provers
           else
             provers
-            |> (if blocking then smart_par_list_map else map) (launch problem)
-            |> exists fst |> rpair state
+            |> (if blocking then smart_par_list_map else map)
+                   (launch problem #> fst)
+            |> max_outcome_code |> rpair state
         end
       fun get_facts label is_appropriate_prop relevance_fudge provers =
         let
@@ -290,24 +306,26 @@
           in
             smts |> map (`(class_of_smt_solver ctxt))
                  |> AList.group (op =)
-                 |> map (launch_provers state (K facts) weight smt_filter o snd)
-                 |> exists fst |> rpair state
+                 |> map (snd #> launch_provers state (K facts) weight smt_filter
+                             #> fst)
+                 |> max_outcome_code |> rpair state
           end
       val launch_full_atps = launch_atps "ATP" (K true) full_atps
       val launch_ueq_atps =
         launch_atps "Unit equational provers" is_unit_equality ueq_atps
       fun launch_atps_and_smt_solvers () =
         [launch_full_atps, launch_ueq_atps, launch_smts]
-        |> smart_par_list_map (fn f => f (false, state) |> K ())
+        |> smart_par_list_map (fn f => f (unknownN, state) |> K ())
         handle ERROR msg => (print ("Error: " ^ msg); error msg)
     in
-      (false, state)
+      (unknownN, state)
       |> (if blocking then
             launch_full_atps #> not auto ? (launch_ueq_atps #> launch_smts)
           else
             (fn p => Future.fork (tap launch_atps_and_smt_solvers) |> K p))
       handle TimeLimit.TimeOut =>
-             (print "Sledgehammer ran out of time."; (false, state))
+             (print "Sledgehammer ran out of time."; (unknownN, state))
     end
+    |> `(fn (outcome_code, _) => outcome_code = someN)
 
 end;

--- a/src/HOL/Tools/try_methods.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/try_methods.ML	Fri May 27 10:30:08 2011 +0200
@@ -6,6 +6,8 @@
 
 signature TRY_METHODS =
 sig
+  val try_methodsN : string
+  val noneN : string
   val auto : bool Unsynchronized.ref
   val try_methods :
     Time.time option -> string list * string list * string list * string list
@@ -16,6 +18,10 @@
 structure Try_Methods : TRY_METHODS =
 struct
 
+val try_methodsN = "try_methods"
+
+val noneN = "none"
+
 val auto = Unsynchronized.ref false
 
 val _ =
@@ -109,7 +115,8 @@
   in
     case do_methods |> Par_List.map (fn f => f auto timeout_opt quad st)
                     |> map_filter I |> sort (int_ord o pairself snd) of
-      [] => (if auto then () else writeln "No proof found."; (false, st))
+      [] => (if auto then () else writeln "No proof found.";
+             (false, (noneN, st)))
     | xs as (s, _) :: _ =>
       let
         val xs = xs |> map (fn (s, n) => (n, hd (space_explode " " s)))
@@ -124,20 +131,18 @@
                 else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^
           "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
       in
-        (true, st |> (if auto then
-                        Proof.goal_message
-                            (fn () => Pretty.chunks [Pretty.str "",
-                                      Pretty.markup Markup.hilite
-                                                    [Pretty.str message]])
-                      else
-                        tap (fn _ => Output.urgent_message message)))
+        (true, (s, st |> (if auto then
+                            Proof.goal_message
+                                (fn () => Pretty.chunks [Pretty.str "",
+                                          Pretty.markup Markup.hilite
+                                                        [Pretty.str message]])
+                          else
+                            tap (fn _ => Output.urgent_message message))))
       end
   end
 
 fun try_methods timeout_opt = fst oo do_try_methods false timeout_opt
 
-val try_methodsN = "try_methods"
-
 fun try_methods_trans quad =
   Toplevel.keep (K () o do_try_methods false (SOME default_timeout) quad
                  o Toplevel.proof_of)
@@ -175,8 +180,8 @@
       "try a combination of proof methods" Keyword.diag
       parse_try_methods_command
 
-val auto_try_methods = do_try_methods true NONE ([], [], [], [])
+fun try_try_methods auto = do_try_methods auto NONE ([], [], [], [])
 
-val setup = Try.register_tool (auto, auto_try_methods)
+val setup = Try.register_tool (try_methodsN, (auto, try_try_methods))
 
 end;

--- a/src/Tools/quickcheck.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/Tools/quickcheck.ML	Fri May 27 10:30:08 2011 +0200
@@ -6,6 +6,10 @@
 
 signature QUICKCHECK =
 sig
+  val quickcheckN: string
+  val genuineN: string
+  val noneN: string
+  val unknownN: string
   val setup: theory -> theory
   (* configuration *)
   val auto: bool Unsynchronized.ref
@@ -61,6 +65,13 @@
 structure Quickcheck : QUICKCHECK =
 struct
 
+val quickcheckN = "quickcheck"
+val quickcheck_paramsN = "quickcheck_params"
+
+val genuineN = "genuine"
+val noneN = "none"
+val unknownN = "unknown"
+
 (* preferences *)
 
 val auto = Unsynchronized.ref false;
@@ -472,10 +483,11 @@
       Pretty.chunks ((Pretty.str (tool_name auto ^ " found a counterexample:\n") ::
         map (fn (s, t) =>
           Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) (rev cex))
-        @ (Pretty.str ("Evaluated terms:\n") ::
-        map (fn (t, u) =>
-          Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1, Syntax.pretty_term ctxt u])
-          (rev eval_terms)));
+        @ (if null eval_terms then []
+           else (Pretty.str ("Evaluated terms:\n") ::
+             map (fn (t, u) =>
+               Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1, Syntax.pretty_term ctxt u])
+               (rev eval_terms))));
 
 fun pretty_report (Report {iterations = iterations, raised_match_errors = raised_match_errors,
     satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}) =
@@ -511,27 +523,6 @@
       (* map (pretty_reports ctxt) (reports_of result) :: *)
       (if Config.get ctxt timing then cons (pretty_timings (timings_of result)) else I) [])
 
-(* automatic testing *)
-
-fun auto_quickcheck state =
-  let
-    val ctxt = Proof.context_of state;
-    val res =
-      state
-      |> Proof.map_context (Config.put report false #> Config.put quiet true)
-      |> try (test_goal (false, false) ([], []) 1);
-  in
-    case res of
-      NONE => (false, state)
-    | SOME (result :: _) => if found_counterexample result then
-        (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "",
-          Pretty.mark Markup.hilite (pretty_counterex ctxt true (response_of result))])) state)
-      else
-        (false, state)
-  end
-
-val setup = Try.register_tool (auto, auto_quickcheck)
-
 (* Isar commands *)
 
 fun read_nat s = case (Library.read_int o Symbol.explode) s
@@ -610,7 +601,8 @@
 
 fun quickcheck_cmd args i state =
   gen_quickcheck args i (Toplevel.proof_of state)
-  |> Pretty.writeln o pretty_counterex_and_reports (Toplevel.context_of state) false;
+  |> Output.urgent_message o Pretty.string_of
+     o pretty_counterex_and_reports (Toplevel.context_of state) false;
 
 val parse_arg =
   Parse.name --
@@ -622,15 +614,47 @@
   Parse.$$$ "[" |-- Parse.list1 parse_arg --| Parse.$$$ "]" || Scan.succeed [];
 
 val _ =
-  Outer_Syntax.command "quickcheck_params" "set parameters for random testing" Keyword.thy_decl
+  Outer_Syntax.command quickcheck_paramsN "set parameters for random testing" Keyword.thy_decl
     (parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args)));
 
 val _ =
-  Outer_Syntax.improper_command "quickcheck" "try to find counterexample for subgoal" Keyword.diag
+  Outer_Syntax.improper_command quickcheckN "try to find counterexample for subgoal" Keyword.diag
     (parse_args -- Scan.optional Parse.nat 1
       >> (fn (args, i) => Toplevel.no_timing o Toplevel.keep (quickcheck_cmd args i)));
 
+(* automatic testing *)
+
+fun try_quickcheck auto state =
+  let
+    val ctxt = Proof.context_of state;
+    val i = 1;
+    val res =
+      state
+      |> Proof.map_context (Config.put report false #> Config.put quiet true)
+      |> try (test_goal (false, false) ([], []) i);
+  in
+    case res of
+      NONE => (unknownN, state)
+    | SOME results =>
+        let
+          val msg = pretty_counterex_and_reports ctxt auto results
+                    |> not auto ? tap (Output.urgent_message o Pretty.string_of)
+        in
+          if exists found_counterexample results then
+            (genuineN,
+             state |> (if auto then
+                         Proof.goal_message (K (Pretty.chunks [Pretty.str "",
+                             Pretty.mark Markup.hilite msg]))
+                       else
+                         I))
+          else
+            (noneN, state)
+        end
+  end
+  |> `(fn (outcome_code, _) => outcome_code = genuineN)
+
+val setup = Try.register_tool (quickcheckN, (auto, try_quickcheck))
+
 end;
 
-
 val auto_quickcheck = Quickcheck.auto;

--- a/src/Tools/solve_direct.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/Tools/solve_direct.ML	Fri May 27 10:30:08 2011 +0200
@@ -10,9 +10,13 @@
 
 signature SOLVE_DIRECT =
 sig
+  val solve_directN: string
+  val someN: string
+  val noneN: string
+  val unknownN: string
   val auto: bool Unsynchronized.ref
   val max_solutions: int Unsynchronized.ref
-  val solve_direct: bool -> Proof.state -> bool * Proof.state
+  val solve_direct: bool -> Proof.state -> bool * (string * Proof.state)
   val setup: theory -> theory
 end;
 
@@ -21,6 +25,9 @@
 
 val solve_directN = "solve_direct";
 
+val someN = "some";
+val noneN = "none";
+val unknownN = "none";
 
 (* preferences *)
 
@@ -74,7 +81,7 @@
   in
     (case try seek_against_goal () of
       SOME (SOME results) =>
-        (true,
+        (someN,
           state |>
            (if auto then
              Proof.goal_message
@@ -85,8 +92,10 @@
             else
               tap (fn _ =>
                 Output.urgent_message (Pretty.string_of (Pretty.chunks (message results))))))
-    | _ => (false, state))
-  end;
+    | SOME NONE => (noneN, state)
+    | NONE => (unknownN, state))
+  end
+  |> `(fn (outcome_code, _) => outcome_code = someN);
 
 val _ =
   Outer_Syntax.improper_command solve_directN
@@ -97,8 +106,6 @@
 
 (* hook *)
 
-val auto_solve_direct = solve_direct true;
-
-val setup = Try.register_tool (auto, auto_solve_direct);
+val setup = Try.register_tool (solve_directN, (auto, solve_direct));
 
 end;

--- a/src/Tools/try.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/Tools/try.ML	Fri May 27 10:30:08 2011 +0200
@@ -6,16 +6,28 @@
 
 signature TRY =
 sig
+  type tool =
+    string * (bool Unsynchronized.ref
+              * (bool -> Proof.state -> bool * (string * Proof.state)))
+
+  val tryN : string
   val auto_time_limit: real Unsynchronized.ref
 
-  val register_tool :
-    bool Unsynchronized.ref * (Proof.state -> bool * Proof.state) -> theory
-    -> theory
+  val register_tool : tool -> theory -> theory
+  val get_tools : theory -> tool list
+  val try_tools : Proof.state -> (string * string) option
 end;
 
 structure Try : TRY =
 struct
 
+type tool =
+  string * (bool Unsynchronized.ref
+            * (bool -> Proof.state -> bool * (string * Proof.state)))
+
+val tryN = "try"
+
+
 (* preferences *)
 
 val auto_time_limit = Unsynchronized.ref 4.0
@@ -31,24 +43,42 @@
 
 structure Data = Theory_Data
 (
-  type T = (bool Unsynchronized.ref * (Proof.state -> bool * Proof.state)) list
+  type T = tool list
   val empty = []
   val extend = I
   fun merge data : T = AList.merge (op =) (K true) data
 )
 
+val get_tools = Data.get
+
 val register_tool = Data.map o AList.update (op =)
 
+(* try command *)
+
+fun try_tools state =
+  get_tools (Proof.theory_of state)
+  |> Par_List.get_some
+         (fn (name, (_, tool)) =>
+             case try (tool false) state of
+               SOME (true, (outcome_code, _)) => SOME (name, outcome_code)
+             | _ => NONE)
+
+val _ =
+  Outer_Syntax.improper_command tryN
+      "try a combination of automatic proving and disproving tools" Keyword.diag
+      (Scan.succeed (Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
+
 
-(* automatic testing *)
+(* automatic try *)
 
-fun run_tools tools state =
-  tools |> map_filter (fn (auto, tool) => if !auto then SOME tool else NONE)
-        |> Par_List.get_some (fn tool =>
-                                 case try tool state of
-                                   SOME (true, state) => SOME state
-                                 | _ => NONE)
-        |> the_default state
+fun auto_try state =
+  get_tools (Proof.theory_of state)
+  |> map_filter (fn (_, (auto, tool)) => if !auto then SOME tool else NONE)
+  |> Par_List.get_some (fn tool =>
+                           case try (tool true) state of
+                             SOME (true, (_, state)) => SOME state
+                           | _ => NONE)
+  |> the_default state
 
 (* Too large values are understood as milliseconds, ensuring compatibility with
    old setting files. No users can possibly in their right mind want the user
@@ -62,8 +92,7 @@
 
 val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
   if interact andalso not (!Toplevel.quiet) andalso !auto_time_limit > 0.0 then
-    TimeLimit.timeLimit (smart_seconds (!auto_time_limit))
-        (run_tools (Data.get (Proof.theory_of state))) state
+    TimeLimit.timeLimit (smart_seconds (!auto_time_limit)) auto_try state
     handle TimeLimit.TimeOut => state
   else
     state))