[isabelle-dev] Quick and dirty evaluation of reals
florian.haftmann at informatik.tu-muenchen.de
Thu Aug 11 09:40:53 CEST 2022
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 228 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev