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.
proper usage of hypotheses for zipperposition's TPTP generation
authordesharna
Tue, 23 Feb 2021 12:20:50 +0100
changeset 73294 f0210642e43f
parent 73293 8b6fa865bac4
child 73295 6c4c37a3ebec
proper usage of hypotheses for zipperposition's TPTP generation
src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Tue Feb 23 10:13:09 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Tue Feb 23 12:20:50 2021 +0100
@@ -550,7 +550,7 @@
      |> extra_options <> "" ? prefix (extra_options ^ " "),
    proof_delims = tstp_proof_delims,
    known_failures = known_szs_status_failures,
-   prem_role = Conjecture,
+   prem_role = Hypothesis,
    best_slices = fn _ =>
      (* FUDGE *)
      [(0.333, (((128, "meshN"), THF (Without_FOOL, Polymorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), zipperposition_blsimp)),
isabelle