Hi,
Thanks a lot. I just tested it with my (hopefully soon to be published)
project using the Real-setup and it works nicely.
One questions: the constant "*" (multiplication) is not defined
for OCaml. Is this intentional or an oversight?
Best,
Achim
On Thu, Aug 11, 2022 at 09:40:53AM +0200, Florian Haftmann wrote:
> Hi all,
>
> starting with an observation by Achim Brucker, I had a look at quick and
> dirty evaluation of reals and realized a lot of issues and deficiencies
> had accumulated over the years.
>
> I tried to consolidate that finally in Isabelle rev. a21debbc7074 and
> AFP rev. eca5cf0e4817
>
> So far there are no observable deficiencies, but heavy users might want
> to check whether everything is still fine.
>
> The matter is quite brittle and so far not systematically tested.
>
> Cheers,
> Florian
>
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
