author | blanchet |
Tue, 14 Feb 2012 20:13:07 +0100 | |
changeset 46481 | c7c85ff6de2a |
parent 46480 | 24990fae5f92 |
child 46482 | f310e9eabf60 |
--- a/src/HOL/Tools/ATP/atp_systems.ML Tue Feb 14 18:58:33 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Feb 14 20:13:07 2012 +0100 @@ -270,7 +270,8 @@ proof_delims = tstp_proof_delims, known_failures = known_szs_status_failures @ - [(TimedOut, "CPU time limit exceeded, terminating")], + [(TimedOut, "CPU time limit exceeded, terminating"), + (GaveUp, "No.of.Axioms")], conj_sym_kind = Axiom, prem_kind = Hypothesis, best_slices = fn ctxt =>