# HG changeset patch # User nipkow # Date 1228396656 -3600 # Node ID f0044cdeb94505358765ac590631c595e38da465 # Parent f6d9e0e0b15322b72a14ff292ecc2e80af06863e NEWS diff -r f6d9e0e0b153 -r f0044cdeb945 NEWS --- a/NEWS Wed Dec 03 21:00:39 2008 -0800 +++ b/NEWS Thu Dec 04 14:17:36 2008 +0100 @@ -55,6 +55,9 @@ * Removed exotic 'token_translation' command. INCOMPATIBILITY, use ML interface instead. +* There is a new lexical item "float" with syntax ["-"] digit+ "." digit+, +without spaces. + *** Pure *** @@ -269,6 +272,9 @@ * HOL/Real/Rational: 'Fract k 0' now equals '0'. INCOMPATIBILITY. +* The real numbers offer decimal input syntax: 12.34 is translated into + 1234/10^4. This translation is not reversed upon output. + * New ML antiquotation @{code}: takes constant as argument, generates corresponding code in background and inserts name of the corresponding resulting ML value/function/datatype constructor binding in place.