Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle 2025-1, RC-1: Problems with Code-Equa...

Email Gateway (Nov 17 2025 at 14:16):

From: "Thiemann, René" <cl-isabelle-users@lists.cam.ac.uk>
Dear all,

the upcoming theory works perfectly fine in Isabelle 2025.

theory Test
imports
Main
"HOL-Analysis.Euclidean_Space"
begin

export_code card (* based on card (set ?xs) = length (remdups ?xs) *)
end

In Isabelle 2025-1, RC-1, there is a problem now:

"Euclidean_Space.euclidean_space_class.Basis" is not a constructor, on left hand side of equation, in theorem:
DIM(?'a) ≡ DIM(?’a)

The problem appeared, when trying to adapt the latest AFP entry Neural Networks from 2025 to 2025-1,
in theory Compass_Digraph where “card” needs to be executable.

Any suggestions?

Best,
René

Email Gateway (Nov 19 2025 at 07:43):

From: Florian Haftmann <florian.haftmann@cit.tum.de>
Hi René,

thanks for reporting this.

This is now restored in
https://isabelle.in.tum.de/repos/isabelle/rev/13e1addb123f

Background: the massive reworking of the code equation bookkeeping
exhibited some dark corners where priorities of equations are not so
clear in the first instance; you hit one of the rare cases where this
actually practically matters (interesting, though, that none of our
existing abundant examples in the AFP already exhibited that).

I plan to iron out those subtle cases, but this is a task after an release.

Cheers,
Florian

Am 17.11.25 um 15:15 schrieb Thiemann, René (via cl-isabelle-users
Mailing List):

Dear all,

the upcoming theory works perfectly fine in Isabelle 2025.

theory Test
imports
Main
"HOL-Analysis.Euclidean_Space"
begin

export_code card (* based on card (set ?xs) = length (remdups ?xs) *)
end

In Isabelle 2025-1, RC-1, there is a problem now:

"Euclidean_Space.euclidean_space_class.Basis" is not a constructor, on left hand side of equation, in theorem:
DIM(?'a) ≡ DIM(?’a)

The problem appeared, when trying to adapt the latest AFP entry Neural Networks from 2025 to 2025-1,
in theory Compass_Digraph where “card” needs to be executable.

Any suggestions?

Best,
René

OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc

Last updated: Dec 02 2025 at 16:32 UTC