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.
use native encoding with Vampire -- modern versions handle types better than the old ones
authorblanchet
Tue, 30 Sep 2014 14:18:07 +0200
changeset 58495 aefcb244423f
parent 58494 ed380b9594b5
child 58496 2ba52ecc4996
use native encoding with Vampire -- modern versions handle types better than the old ones
src/HOL/Tools/ATP/atp_systems.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Sep 30 14:18:07 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Sep 30 14:18:07 2014 +0200
@@ -536,7 +536,7 @@
    best_slices = fn ctxt =>
      (* FUDGE *)
      (if is_vampire_beyond_1_8 () then
-        [(0.333, (((500, meshN), vampire_tff0, "mono_guards??", combs_or_liftingN, false), sosN)),
+        [(0.333, (((500, meshN), vampire_tff0, "mono_native", combs_or_liftingN, false), sosN)),
          (0.333, (((150, meshN), vampire_tff0, "poly_tags??", combs_or_liftingN, false), sosN)),
          (0.334, (((50, meshN), vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN))]
       else
isabelle