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.
there won't be an E version 2.7
authorblanchet
Wed, 01 Mar 2023 08:00:51 +0100
changeset 77431 cdf5f392ea78
parent 77430 51dac6fcdd0e
child 77432 e51aa922079a
there won't be an E version 2.7
src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Wed Mar 01 08:00:51 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Wed Mar 01 08:00:51 2023 +0100
@@ -195,8 +195,8 @@
    good_slices =
      let
        val (format, type_enc, lam_trans, extra_options) =
-         if string_ord (getenv "E_VERSION", "2.7") <> LESS then
-           (* '$ite' support appears to be buggy *)
+         if string_ord (getenv "E_VERSION", "3.0") <> LESS then
+           (* '$ite' support appears to be unsound. *)
            (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, "--auto-schedule=4 --serialize-schedule=true --demod-under-lambda=true")
          else if string_ord (getenv "E_VERSION", "2.6") <> LESS then
            (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, "--auto-schedule")
isabelle