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