Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
propagate right result when enough proofs have been found
authorblanchet
Tue, 01 Feb 2022 17:11:26 +0100
changeset 75056 04a4881ff0fd
parent 75055 c84a20e9b00f
child 75057 79b4e711d6a2
propagate right result when enough proofs have been found
src/HOL/Tools/Sledgehammer/sledgehammer.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Feb 01 16:16:50 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Feb 01 17:11:26 2022 +0100
@@ -445,7 +445,7 @@
                    if Synchronized.value found_proofs < max_proofs then
                      launch problem slice prover
                    else
-                     (SH_Unknown, ""))
+                     (SH_None, ""))
                  prover_slices
                |> max_outcome)
           end
isabelle