--- 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.