[isabelle-dev] »real« considered harmful

[Florian Haftmann]

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
work).

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

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