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