(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://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20070903/d5f87c38/attachment.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://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20070903/d5f87c38/attachment.pgp
