[isabelle-dev] Quick and dirty evaluation of reals

[Achim D. Brucker]

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
>