[isabelle-dev] quickcheck on type real

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Mon Sep 3 08:07:07 CEST 2007

(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?


-------------- 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>

More information about the isabelle-dev mailing list