Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
take out Waldmeister from default for now -- success rate too low on Judgment Day
authorblanchet
Fri, 27 May 2011 10:30:07 +0200
changeset 42997 038bb26d74b0
parent 42996 29be053ec75b
child 42998 1c80902d0456
take out Waldmeister from default for now -- success rate too low on Judgment Day
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 27 10:30:07 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 27 10:30:07 2011 +0200
@@ -183,7 +183,7 @@
 (* The first ATP of the list is used by Auto Sledgehammer. Because of the low
    timeout, it makes sense to put SPASS first. *)
 fun default_provers_param_value ctxt =
-  [spassN, eN, vampireN, sine_eN, waldmeisterN, SMT_Solver.solver_name_of ctxt]
+  [spassN, eN, vampireN, sine_eN, SMT_Solver.solver_name_of ctxt]
   |> map_filter (remotify_prover_if_not_installed ctxt)
   |> avoid_too_many_local_threads ctxt (Multithreading.max_threads_value ())
   |> implode_param
isabelle