changeset 75049 | 8ce2469920bf |
parent 75047 | 7d2a5d1f09af |
child 75051 | 1a8f6cb5efd6 |
--- 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 =