Incorrect result from signed right-shift when using Code_Target_Numeral

[Daniel Matichuk]

Some quick tests with the code generator indicate that this revision seems
to have resolved the issue (compiled with GMP enabled, using arm64_32).

On Fri, Dec 5, 2025 at 1:58 PM Makarius <makarius at sketis.net> wrote:

> 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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20251205/3ce4525b/attachment.htm>