--- 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.
--- 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}
--- 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