[isabelle-dev] quickcheck on type real

[Florian Haftmann]

(1) I discovered a slip in the implementation of Rat.inv which did not
normalize negative rats; this might explain the strange behaviour of
equality (fixed in CVS).

(2) I strongly support Amine's issue: all code generator frameworks
should use the verified rational numbers.  Why I have refrained so far
from doing this is I would have to drop the existing implementation of
rational reals entirely for Stefan's framework.  Anyone objecting to this?

Florian

-------------- next part --------------
A non-text attachment was scrubbed...
Name: florian.haftmann.vcf
Type: text/x-vcard
Size: 654 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20070903/d5f87c38/attachment-0002.vcf>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 185 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20070903/d5f87c38/attachment.sig>