[Afp-submit] AFP entry Neural_Networks

[Makarius]

On 20/11/2025 14:21, Achim D. Brucker wrote:
> 
> The actually value stored is 0.070820772089064121246337890625 (decoding it 
> "manually", following the standard). Trying to print it in a small C programm 
> gives 0.00708207720890641212, which seems to be the offical decimal 
> represenation according to the standard. IEEE754  is not easy ...
Note that there have been changes on reals in polyml-5.9.1 (Isabelle2025) to 
polyml-5.9.2 (Isabelle2025-1).

An example changeset by David Matthews is here 
https://github.com/polyml/polyml/commit/cc497eb585b0

Maybe someone who understands the fine points can check if it has become more 
correct or less correct.


	Makarius