author | blanchet |
Thu, 10 May 2012 10:07:40 +0200 | |
changeset 47899 | 493d70c63fd6 |
parent 47898 | 6213900d6d5f |
child 47900 | 6440a74b2f62 |
--- a/src/HOL/Tools/ATP/atp_systems.ML Thu May 10 10:07:40 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Thu May 10 10:07:40 2012 +0200 @@ -337,7 +337,7 @@ [(TimedOut, "CPU time limit exceeded, terminating"), (GaveUp, "No.of.Axioms")], conj_sym_kind = Axiom, - prem_kind = Definition (* motivated by "isabelle tptp_sledgehammer" tool *), + prem_kind = Hypothesis, best_slices = fn ctxt => (* FUDGE *) [(0.667, (false, ((150, leo2_thf0, "mono_native_higher", keep_lamsN, false), sosN))),