Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
changeset 82620 2d854f1cd830
parent 82202 a1f85f579a07 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Sun May 11 12:05:10 2025 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon May 12 13:02:52 2025 +0200
@@ -82,7 +82,7 @@
      used_from : fact list,
      preferred_methss : proof_method * proof_method list list,
      run_time : Time.time,
-     message : (unit -> (Pretty.T * stature) list * (proof_method * play_outcome)) -> string}
+     message : ((Pretty.T * stature) list * (proof_method * play_outcome)) option -> string}
 
   type prover = params -> prover_problem -> prover_slice -> prover_result
 
@@ -210,7 +210,7 @@
    used_from : fact list,
    preferred_methss : proof_method * proof_method list list,
    run_time : Time.time,
-   message : (unit -> (Pretty.T * stature) list * (proof_method * play_outcome)) -> string}
+   message : ((Pretty.T * stature) list * (proof_method * play_outcome)) option -> string}
 
 type prover = params -> prover_problem -> prover_slice -> prover_result
isabelle