tuned punctuation
authorblanchet
Tue, 01 Feb 2022 11:52:40 +0100
changeset 75049 8ce2469920bf
parent 75048 e926618f9474
child 75050 632c9ae415fa
tuned punctuation
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- 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 =