--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Thu Apr 24 09:16:33 2025 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Thu Apr 24 14:25:12 2025 +0200
@@ -44,6 +44,7 @@
val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
val string_of_play_outcome : play_outcome -> string
val play_outcome_ord : play_outcome ord
+ val try_command_line : string -> play_outcome -> string -> string
val one_line_proof_text : one_line_params -> string
end;