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