--- a/NEWS Thu Dec 04 14:43:33 2008 +0100
+++ b/NEWS Thu Dec 04 14:44:07 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 ***
@@ -281,6 +284,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.