Incorrect result from signed right-shift when using Code_Target_Numeral
Makarius
makarius at sketis.net
Sun Dec 7 00:03:17 CET 2025
The isabelle-release repository now has this changeset:
changeset: 83717:f274b63c5b44
tag: tip
user: wenzelm
date: Sat Dec 06 23:51:17 2025 +0100
files: Admin/components/components.sha1 Admin/components/main
description:
update to polyml-5.9.2-2 version ccd3e3717f72 from branch fixes-5.9.2, which
provides a corrected implementation of IntInf right shift;
keep redundant checks for further testing;
The plan is to publish it in Isabelle2025-1-RC4 next week (probably Monday),
and remove the redundant check for the final release.
The changeset will return to isabelle-dev shortly after Isabelle2025-1-RC4.
Makarius
More information about the isabelle-dev
mailing list