Incorrect result from signed right-shift when using Code_Target_Numeral

Makarius makarius at sketis.net
Fri Dec 5 22:58:51 CET 2025


On 05/12/2025 22:42, Makarius wrote:
> 
> Right now our main problem is that 64eb08b0a4bc is on top of "latest" Poly/ML 
> development and experiments. Thus it does not quite work for Isabelle yet, 
> especially HOL-Codegenerator_Test. For the release the change needs to sit on 
> top of official v5.9.2.

I now see 638379c583a5, and that looks fine so far in a quick test of 
HOL-Codegenerator_Test ...


	Makarius



More information about the isabelle-dev mailing list