# HG changeset patch
# User haftmann
# Date 1228398247 -3600
# Node ID 71a7f76b522d8014156add25e55c9ace09b9c2f4
# Parent  f0044cdeb94505358765ac590631c595e38da465# Parent  1de908189869ea943fd0ea992cb18b94b48cf9a8
merged

diff -r 1de908189869 -r 71a7f76b522d NEWS
--- 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.