minor slice tweaking (swapped two slices to move polymorphic encoding up a bit)
authorblanchet
Wed May 16 18:16:51 2012 +0200 (2012-05-16)
changeset 47931406d1df3787e
parent 47930 c06aa331bb76
child 47932 ce4178e037a7
minor slice tweaking (swapped two slices to move polymorphic encoding up a bit)
src/HOL/Tools/ATP/atp_systems.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Wed May 16 18:16:51 2012 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed May 16 18:16:51 2012 +0200
     1.3 @@ -417,10 +417,10 @@
     1.4        (0.1667, (false, ((500, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H2SOS))),
     1.5        (0.1666, (false, ((50, DFG DFG_Sorted,  "mono_native", liftingN, true), spass_new_H2))),
     1.6        (0.1000, (false, ((250, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2NuVS0))),
     1.7 -      (0.1000, (false, ((100, DFG DFG_Sorted, "mono_native", combs_and_liftingN, true), spass_new_H2NuVS0))),
     1.8        (0.1000, (false, ((1000, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H1SOS))),
     1.9        (0.1000, (false, ((150, DFG DFG_Sorted, "poly_guards??", liftingN, false), spass_new_H2NuVS0Red2))),
    1.10 -      (0.1000, (false, ((300, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2SOS)))]}
    1.11 +      (0.1000, (false, ((300, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2SOS))),
    1.12 +      (0.1000, (false, ((100, DFG DFG_Sorted, "mono_native", combs_and_liftingN, true), spass_new_H2NuVS0)))]}
    1.13  
    1.14  val spass_new = (spass_newN, fn () => spass_new_config)
    1.15