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.
put faster proof methods first
authorblanchet
Wed, 30 Jul 2014 23:52:56 +0200
changeset 57724 9ea51eddf81c
parent 57723 668322cd58f4
child 57725 a297879fe5b8
put faster proof methods first
src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Wed Jul 30 23:52:56 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Wed Jul 30 23:52:56 2014 +0200
@@ -184,9 +184,9 @@
   | _ => "Try this")
 
 fun bunch_of_proof_methods smt_proofs needs_full_types desperate_lam_trans =
-  [Metis_Method (if needs_full_types then SOME full_typesN else NONE, NONE),
-   Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Meson_Method, Blast_Method,
-   Linarith_Method, Presburger_Method] @
+  [Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Meson_Method,
+   Metis_Method (if needs_full_types then SOME full_typesN else NONE, NONE),
+   Force_Method, Linarith_Method, Presburger_Method] @
   (if needs_full_types then
      [Metis_Method (SOME really_full_type_enc, NONE),
       Metis_Method (SOME full_typesN, SOME desperate_lam_trans),
isabelle