1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Mar 27 16:59:13 2012 +0300
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Mar 27 16:59:13 2012 +0300
     1.3 @@ -406,6 +406,7 @@
     1.4  
     1.5  val spass_old = (spass_oldN, spass_old_config)
     1.6  
     1.7 +val spass_new_H1SOS = "-Heuristic=1 -SOS"
     1.8  val spass_new_H2 = "-Heuristic=2"
     1.9  val spass_new_H2SOS = "-Heuristic=2 -SOS"
    1.10  val spass_new_H2NuVS0 = "-Heuristic=2 -RNuV=1 -Sorts=0"
    1.11 @@ -429,9 +430,9 @@
    1.12        (0.1666, (false, ((50, DFG DFG_Sorted,  "mono_native", liftingN, true), spass_new_H2))),
    1.13        (0.1000, (false, ((250, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2NuVS0))),
    1.14        (0.1000, (false, ((100, DFG DFG_Sorted, "mono_native", combs_and_liftingN, true), spass_new_H2NuVS0))),
    1.15 -      (0.1000, (false, ((300, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2SOS))),
    1.16 +      (0.1000, (false, ((1000, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H1SOS))),
    1.17        (0.1000, (false, ((150, DFG DFG_Sorted, "poly_guards??", liftingN, false), spass_new_H2NuVS0Red2))),
    1.18 -      (0.1000, (false, ((400, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H2)))]}
    1.19 +      (0.1000, (false, ((300, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2SOS)))]}
    1.20  
    1.21  val spass_new = (spass_newN, spass_new_config)
    1.22