# HG changeset patch # User blanchet # Date 1412079487 -7200 # Node ID aefcb244423fae1e0c54ad200b81646c8ab94ff2 # Parent ed380b9594b5c2d4bbb89bfdb2451d73213e3a54 use native encoding with Vampire -- modern versions handle types better than the old ones diff -r ed380b9594b5 -r aefcb244423f src/HOL/Tools/ATP/atp_systems.ML --- 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