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.
change order of default ATPs;
authorblanchet
Sat, 11 Sep 2010 10:22:52 +0200
changeset 39319 da4e98cb2005
parent 39318 ad9a1f9b0558
child 39320 5d578004be23
change order of default ATPs; put SPASS first so that it's picked up by Auto Sledgehammer
src/HOL/Tools/ATP/atp_systems.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/ATP/atp_systems.ML	Sat Sep 11 10:21:52 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Sat Sep 11 10:22:52 2010 +0200
@@ -303,9 +303,11 @@
 fun maybe_remote (name, config) =
   name |> not (is_installed config) ? remotify_name
 
+(* The first prover of the list is used by Auto Sledgehammer. Because of the low
+   timeout, it makes sense to put SPASS first. *)
 fun default_atps_param_value () =
-  space_implode " " ([maybe_remote e] @
-                     (if is_installed (snd spass) then [fst spass] else []) @
+  space_implode " " ((if is_installed (snd spass) then [fst spass] else []) @
+                     [maybe_remote e] @
                      [if forall (is_installed o snd) [e, spass] then
                         remotify_name (fst vampire)
                       else
isabelle