--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Wed Jan 05 15:35:23 2022 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Fri Jan 07 08:50:12 2022 +0100
@@ -302,7 +302,7 @@
if string_ord (getenv "E_VERSION", "2.7") <> LESS then
(THF (Monomorphic, {with_ite = true, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN)
else if string_ord (getenv "E_VERSION", "2.6") <> LESS then
- (THF (Monomorphic, {with_ite = true, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN)
+ (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN)
else
(THF (Monomorphic, {with_ite = false, with_let = false}, THF_Lambda_Free), "mono_native_higher", combsN)
in
--- a/src/HOL/Wellfounded.thy Wed Jan 05 15:35:23 2022 +0000
+++ b/src/HOL/Wellfounded.thy Fri Jan 07 08:50:12 2022 +0100
@@ -56,6 +56,12 @@
obtains "(x, a) \<notin> r"
by (drule wf_not_sym[OF assms])
+lemma wf_imp_asym: "wf r \<Longrightarrow> asym r"
+ by (auto intro: asymI elim: wf_asym)
+
+lemma wfP_imp_asymp: "wfP r \<Longrightarrow> asymp r"
+ by (rule wf_imp_asym[to_pred])
+
lemma wf_not_refl [simp]: "wf r \<Longrightarrow> (a, a) \<notin> r"
by (blast elim: wf_asym)
@@ -68,6 +74,9 @@
assumes "wf r" shows "irrefl r"
using wf_irrefl [OF assms] by (auto simp add: irrefl_def)
+lemma wfP_imp_irreflp: "wfP r \<Longrightarrow> irreflp r"
+ by (rule wf_imp_irrefl[to_pred])
+
lemma wf_wellorderI:
assumes wf: "wf {(x::'a::ord, y). x < y}"
and lin: "OFCLASS('a::ord, linorder_class)"