Email Gateway (Oct 05 2026 at 22:31): Email Gateway (Oct 05 2026 at 22:31):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Subject: [isabelle] Isabelle2026-RC3 missing "verit" facts that worked in Isabelle 2026-Rc0
I downloaded Isabelle2026-RC3 and tried it on something I had been working on.
Some proofs that previously worked do not, now, due to facts that seem no longer
to be known. I tried to repair one of these using sledgehammer (which was probably
what I used to find the first proof), but it fails.
- Gene Stark
lemma rank_uminus [simp]:
shows "ρ[- f] = ρ[f]"
by (metis nle_le pointwise_op_def rank_pointwise_op uminus_FR_def verit_minus_simplify(4))
"verit_minus_simplify(4)" is no longer known
lemma leq_FR_antisymmetric:
assumes "leq_FR f g ∧ leq_FR g f"
shows "f = g"
unfolding leq_FR_def
by (meson antisym_conv1 assms eq_iff_eq_val leq_FR_def order_less_irrefl verit_la_disequality)
"verit_la_disequality" is no longer known
lemma leq_FR_pointwise_op:
assumes "⋀x y. x ≤ y ⟹ h x ≤ h y"
and "leq_FR f g"
shows "leq_FR (pointwise_op h f) (pointwise_op h g)"
using assms
by (metis leq_FR_def val_pointwise_op verit_comp_simplify1(2))
"verit_comp_simplify1(2)" is no longer known
On 10/5/26 17:21, Makarius wrote:
Dear Isabelle users,
the Isabelle2026 release train has arrived at station "RC3", see also https://sketis.net/2026/release-candidates-for-
isabelle2026 for details. A few minor technical problems still need to be sorted out, and some documentations needs
final updates.The main Isabelle website is https://isabelle.in.tum.de/website-Isabelle2026-RC3
We now also have regular afp-2026 to go with it: https://foss.heptapod.net/isa-afp/afp-2026
Any feedback about Isabelle release candidates should be posted with a meaningful Mail subject, not just a clone of this
announcement.Makarius
Email Gateway (Oct 06 2026 at 00:26):From: "Lammich, Peter (UT-EEMCS)" <cl-isabelle-users@lists.cam.ac.uk>
Subject: [isabelle] Isabelle2026-RC3 missing "verit" facts that worked in Isabelle 2026-Rc0
Hello
Yes, sledgehammer unfortunately sometimes selects obviously internal names for proofs. This causes brittle proofs. In most cases sledgehammering again works. Last resort: find out the lemma statement using the old version, and then use find theorems to find it in the new version
Peter
Sent from Outlook for Android<https://aka.ms/AAb9ysg>
From: cl-isabelle-users-request@lists.cam.ac.uk <cl-isabelle-users-request@lists.cam.ac.uk> on behalf of Eugene W. Stark <isabelle-users@starkeffect.com>
Sent: Monday, 05 October 2026 23:31:34
To: cl-isabelle-users@lists.cam.ac.uk <cl-isabelle-users@lists.cam.ac.uk>
Subject: [isabelle] Isabelle2026-RC3 missing "verit" facts that worked in Isabelle 2026-Rc0
I downloaded Isabelle2026-RC3 and tried it on something I had been working on.
Some proofs that previously worked do not, now, due to facts that seem no longer
to be known. I tried to repair one of these using sledgehammer (which was probably
what I used to find the first proof), but it fails.
- Gene Stark
lemma rank_uminus [simp]:
shows "ρ[- f] = ρ[f]"
by (metis nle_le pointwise_op_def rank_pointwise_op uminus_FR_def verit_minus_simplify(4))
"verit_minus_simplify(4)" is no longer known
lemma leq_FR_antisymmetric:
assumes "leq_FR f g ∧ leq_FR g f"
shows "f = g"
unfolding leq_FR_def
by (meson antisym_conv1 assms eq_iff_eq_val leq_FR_def order_less_irrefl verit_la_disequality)
"verit_la_disequality" is no longer known
lemma leq_FR_pointwise_op:
assumes "⋀x y. x ≤ y ⟹ h x ≤ h y"
and "leq_FR f g"
shows "leq_FR (pointwise_op h f) (pointwise_op h g)"
using assms
by (metis leq_FR_def val_pointwise_op verit_comp_simplify1(2))
"verit_comp_simplify1(2)" is no longer known
On 10/5/26 17:21, Makarius wrote:
Dear Isabelle users,
the Isabelle2026 release train has arrived at station "RC3", see also https://sketis.net/2026/release-candidates-for-
isabelle2026 for details. A few minor technical problems still need to be sorted out, and some documentations needs
final updates.The main Isabelle website is https://isabelle.in.tum.de/website-Isabelle2026-RC3
We now also have regular afp-2026 to go with it: https://foss.heptapod.net/isa-afp/afp-2026
Any feedback about Isabelle release candidates should be posted with a meaningful Mail subject, not just a clone of this
announcement.Makarius
Email Gateway (Oct 08 2026 at 16:00):From: Hanna Elif Lachnitt <cl-isabelle-users@lists.cam.ac.uk>
Subject: [isabelle] Isabelle2026-RC3 missing "verit" facts that worked in Isabelle 2026-Rc0
Hi Gene,
All the facts have been renamed from verit_<name> to alethe_<name>. The veriT solver's output format has been refined and is now called Alethe and also used by cvc5.
To avoid issues like this one in the future, the lemmas have now been marked as [no_atp], which is why Sledgehammer won't find them.
Best,
Hanna Lachnitt
Message-ID: <354c4b1a-a8cf-4b99-a4b6-c55167bafcd9@starkeffect.com>
Date: Mon, 5 Oct 2026 18:31:34 -0400
From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Subject: [isabelle] Isabelle2026-RC3 missing "verit" facts that worked in
Isabelle 2026-Rc0
I downloaded Isabelle2026-RC3 and tried it on something I had been working on.
Some proofs that previously worked do not, now, due to facts that seem no
longer
to be known. I tried to repair one of these using sledgehammer (which was
probably
what I used to find the first proof), but it fails.
- Gene Stark
lemma rank_uminus [simp]:
shows "ρ[- f] = ρ[f]"
by (metis nle_le pointwise_op_def rank_pointwise_op uminus_FR_def
verit_minus_simplify(4))
"verit_minus_simplify(4)" is no longer known
lemma leq_FR_antisymmetric:
assumes "leq_FR f g ∧ leq_FR g f"
shows "f = g"
unfolding leq_FR_def
by (meson antisym_conv1 assms eq_iff_eq_val leq_FR_def order_less_irrefl
verit_la_disequality)
"verit_la_disequality" is no longer known
lemma leq_FR_pointwise_op:
assumes "⋀x y. x ≤ y ⟹ h x ≤ h y"
and "leq_FR f g"
shows "leq_FR (pointwise_op h f) (pointwise_op h g)"
using assms
by (metis leq_FR_def val_pointwise_op verit_comp_simplify1(2))
"verit_comp_simplify1(2)" is no longer known
Last updated: Oct 08 2026 at 21:07 UTC