1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:46 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:46 2012 +0200
     1.3 @@ -29,6 +29,10 @@
     1.4  open Sledgehammer_MaSh
     1.5  open Sledgehammer_Run
     1.6  
     1.7 +val cvc3N = "cvc3"
     1.8 +val yicesN = "yices"
     1.9 +val z3N = "z3"
    1.10 +
    1.11  val runN = "run"
    1.12  val minN = "min"
    1.13  val messagesN = "messages"
    1.14 @@ -220,10 +224,9 @@
    1.15  val max_default_remote_threads = 4
    1.16  
    1.17  (* The first ATP of the list is used by Auto Sledgehammer. Because of the low
    1.18 -   timeout, it makes sense to put SPASS first. *)
    1.19 +   timeout, it makes sense to put E first. *)
    1.20  fun default_provers_param_value ctxt =
    1.21 -  [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, e_sineN,
    1.22 -   waldmeisterN]
    1.23 +  [eN, spassN, vampireN, z3N, e_sineN, waldmeisterN, yicesN, cvc3N]
    1.24    |> map_filter (remotify_prover_if_not_installed ctxt)
    1.25    |> avoid_too_many_threads ctxt (Multithreading.max_threads_value (),
    1.26                                    max_default_remote_threads)