--- a/NEWS Thu Dec 04 08:47:45 2008 -0800
+++ b/NEWS Thu Dec 04 09:12:41 2008 -0800
@@ -55,9 +55,24 @@
* Removed exotic 'token_translation' command. INCOMPATIBILITY, use ML
interface instead.
+* There is a new lexical item "float" with syntax ["-"] digit+ "." digit+,
+without spaces.
+
*** Pure ***
+* Type Binding.T gradually replaces formerly used type bstring for names
+to be bound. Name space interface for declarations has been simplified:
+
+ NameSpace.declare: NameSpace.naming
+ -> Binding.T -> NameSpace.T -> string * NameSpace.T
+ NameSpace.bind: NameSpace.naming
+ -> Binding.T * 'a -> 'a NameSpace.table -> string * 'a NameSpace.table
+ (*exception Symtab.DUP*)
+
+See further modules src/Pure/General/binding.ML and
+src/Pure/General/name_space.ML
+
* Module moves in repository:
src/Pure/Tools/value.ML ~> src/Tools/
src/Pure/Tools/quickcheck.ML ~> src/Tools/
@@ -269,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.