changeset 69989 | bcba61d92558 |
parent 67399 | eab6ce8368fa |
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy Tue Mar 26 13:25:32 2019 +0100 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy Tue Mar 26 13:45:46 2019 +0100 @@ -931,7 +931,6 @@ fun biggest_hyp_first_tac i = fn st => let val results = TERMFUN biggest_hypothesis (SOME i) st -val _ = tracing ("result=" ^ @{make_string} results) in if null results then no_tac st else