# HG changeset patch
# User blanchet
# Date 1660753210 -7200
# Node ID 5f7d22354a658c9eae34b651fec5a27ca2c7448a
# Parent  8bfad7bc74cbacf96483ead10ac2a74afbf33104
tweaked generation of Isar proofs

diff -r 8bfad7bc74cb -r 5f7d22354a65 NEWS
--- a/NEWS	Wed Aug 17 15:09:53 2022 +0200
+++ b/NEWS	Wed Aug 17 18:20:10 2022 +0200
@@ -146,6 +146,8 @@
   - Added support for TX0 and TX1 TPTP formats and $ite/$let expressions
     in TH0 and TH1.
   - Added support for cvc5.
+  - Generate Isar proofs by default when and only when the one-liner proof
+    fails to replay and the Isar proof succeeds.
   - Replaced option "sledgehammer_atp_dest_dir" by
     "sledgehammer_atp_problem_dest_dir", for problem files, and
     "sledgehammer_atp_proof_dest_dir", for proof files. Minor INCOMPATIBILITY.
diff -r 8bfad7bc74cb -r 5f7d22354a65 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Wed Aug 17 15:09:53 2022 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Wed Aug 17 18:20:10 2022 +0200
@@ -1129,9 +1129,9 @@
 \opsmart{isar\_proofs}{no\_isar\_proofs}
 Specifies whether Isar proofs should be output in addition to one-line proofs.
 The construction of Isar proof is still experimental and may sometimes fail;
-however, when they succeed they are usually faster and more intelligible than
-one-line proofs. If the option is set to \textit{smart} (the default), Isar
-proofs are only generated when no working one-line proof is available.
+however, when they succeed they can be faster and sometimes more intelligible
+than one-line proofs. If the option is set to \textit{smart} (the default), Isar
+proofs are generated only when no working one-line proof is available.
 
 \opdefault{compress}{int}{smart}
 Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs}
diff -r 8bfad7bc74cb -r 5f7d22354a65 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Aug 17 15:09:53 2022 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Aug 17 18:20:10 2022 +0200
@@ -494,9 +494,12 @@
                   (if do_preplay then [string_of_play_outcome play_outcome] else [])
               in
                 one_line_proof_text ctxt 0 one_line_params ^
-                "\n\nIsar proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^
-                Active.sendback_markup_command
-                  (string_of_isar_proof ctxt subgoal subgoal_count isar_proof)
+                (if isar_proofs <> NONE orelse (case play_outcome of Played _ => true | _ => false) then
+                   "\n\nIsar proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^
+                   Active.sendback_markup_command
+                     (string_of_isar_proof ctxt subgoal subgoal_count isar_proof)
+                 else
+                   "")
               end)
           end
       end