[isabelle-dev] floats

[Tobias Nipkow]

* The real numbers now offer decimal input syntax: 12.34 is translated into
  1234/10^4. This translation is not reversed upon output.

If somebody wants to develop this further, they should feel free to do so.

Tobias