On 31/01/2025 20:18, Florian Haftmann wrote: > See now https://foss.heptapod.net/isa-afp/afp-devel/-/commit/ > b1295207946a90e2c347c43f08518f4e222ac7d3 Great. Makarius