* 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