> I just discovered that another last minute "FIXME" has changed the
> hierarchy of rings in Isabelle2007 such that "real" is not of sort
> "lordered_ring" any more. More generally, "ordered_ring" is not an
> "lordered_ring" any more. This is pretty unfortunate as it renders the
> whole HOL-Complex-Matrix package in Isabelle 2007 garbage. Maybe in the
> future one should refrain from last minute fixes which one does not
> fully understand.
This change is due to the changed and unified formalization of lattices
in HOL. Providing an instance real :: lattice should be sufficient.
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/20071205/1ed2aa42/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/20071205/1ed2aa42/attachment.pgp
