[isabelle-dev] Quick and dirty evaluation of reals

[Florian Haftmann]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20220811/bc150211/attachment.sig>