author | blanchet |
Tue, 01 Feb 2022 11:52:40 +0100 | |
changeset 75049 | 8ce2469920bf |
parent 75048 | e926618f9474 |
child 75050 | 632c9ae415fa |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Feb 01 11:51:41 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Feb 01 11:52:40 2022 +0100 @@ -480,7 +480,7 @@ end) else one_line_params) ^ - (if isar_proofs = SOME true then "\n(No Isar proof available.)" else "") + (if isar_proofs = SOME true then "\n(No Isar proof available)" else "") | (_, num_steps) => let val msg =