[isabelle-dev] »real« considered harmful

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu Aug 6 11:05:47 CEST 2015

A conclusion of what I have understood so far:
* A new »of_float :: float => 'a::field« is provided (btw. »float« could
be also constructed from the rationals rather than the reals).
* »real« is restricted to »real :: nat => real« (which corresponds
nicely to »int :: nat => int«).
* The special case real [ereal] is renamed, e.g. »the_real :: ereal =>
real« (cf. enat)
* Other occurences of real are substituted (if coercions do not save the



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20150806/b2d5176c/attachment.asc>

More information about the isabelle-dev mailing list