src/HOL/Tools/ATP/atp_systems.ML
changeset 47931 406d1df3787e
parent 47916 d21c91239737
child 47948 0524790d2112
equal deleted inserted replaced
47930:c06aa331bb76 47931:406d1df3787e
   415      (* FUDGE *)
   415      (* FUDGE *)
   416      [(0.1667, (false, ((150, DFG DFG_Sorted, "mono_native", combsN, true), ""))),
   416      [(0.1667, (false, ((150, DFG DFG_Sorted, "mono_native", combsN, true), ""))),
   417       (0.1667, (false, ((500, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H2SOS))),
   417       (0.1667, (false, ((500, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H2SOS))),
   418       (0.1666, (false, ((50, DFG DFG_Sorted,  "mono_native", liftingN, true), spass_new_H2))),
   418       (0.1666, (false, ((50, DFG DFG_Sorted,  "mono_native", liftingN, true), spass_new_H2))),
   419       (0.1000, (false, ((250, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2NuVS0))),
   419       (0.1000, (false, ((250, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2NuVS0))),
   420       (0.1000, (false, ((100, DFG DFG_Sorted, "mono_native", combs_and_liftingN, true), spass_new_H2NuVS0))),
       
   421       (0.1000, (false, ((1000, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H1SOS))),
   420       (0.1000, (false, ((1000, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H1SOS))),
   422       (0.1000, (false, ((150, DFG DFG_Sorted, "poly_guards??", liftingN, false), spass_new_H2NuVS0Red2))),
   421       (0.1000, (false, ((150, DFG DFG_Sorted, "poly_guards??", liftingN, false), spass_new_H2NuVS0Red2))),
   423       (0.1000, (false, ((300, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2SOS)))]}
   422       (0.1000, (false, ((300, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2SOS))),
       
   423       (0.1000, (false, ((100, DFG DFG_Sorted, "mono_native", combs_and_liftingN, true), spass_new_H2NuVS0)))]}
   424 
   424 
   425 val spass_new = (spass_newN, fn () => spass_new_config)
   425 val spass_new = (spass_newN, fn () => spass_new_config)
   426 
   426 
   427 val spass =
   427 val spass =
   428   (spassN, fn () => if is_new_spass_version () then spass_new_config
   428   (spassN, fn () => if is_new_spass_version () then spass_new_config