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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
