# HG changeset patch
# User blanchet
# Date 1359909093 -3600
# Node ID a4a32c1d2866d899df7ac49b338e3083da044896
# Parent  6a760e7f693394a549c7177bafd268f579804c8b
tuned slicing (E-MaLeS and E-Par)

diff -r 6a760e7f6933 -r a4a32c1d2866 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Sat Feb 02 17:25:55 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Sun Feb 03 17:31:33 2013 +0100
@@ -362,7 +362,10 @@
    prem_role = Conjecture,
    best_slices =
      (* FUDGE *)
-     K [(1.0, (((1000, ""), FOF, "poly_guards??", combsN, false), ""))],
+     K [(0.25, (((500, meshN), FOF, "mono_guards??", combs_or_liftingN, false), "")),
+        (0.25, (((150, meshN), FOF, "poly_tags??", combs_or_liftingN, false), "")),
+        (0.25, (((50, meshN), FOF, "mono_tags??", combs_or_liftingN, false), "")),
+        (0.25, (((1000, meshN), FOF, "poly_guards??", combsN, false), ""))],
    best_max_mono_iters = default_max_mono_iters,
    best_max_new_mono_instances = default_max_new_mono_instances}