NEWS
changeset 30399 a4772a650b4e
parent 30395 f3103bd2b167
child 30415 9501af91c4a3
     1.1 --- a/NEWS	Mon Mar 09 21:26:13 2009 +0100
     1.2 +++ b/NEWS	Mon Mar 09 22:43:25 2009 +0100
     1.3 @@ -624,13 +624,13 @@
     1.4  
     1.5  * More systematic treatment of long names, abstract name bindings, and
     1.6  name space operations.  Basic operations on qualified names have been
     1.7 -move from structure NameSpace to Long_Name, e.g.  Long_Name.base_name,
     1.8 +move from structure NameSpace to Long_Name, e.g. Long_Name.base_name,
     1.9  Long_Name.append.  Old type bstring has been mostly replaced by
    1.10  abstract type binding (see structure Binding), which supports precise
    1.11 -qualification (by packages and local theory), and proper tracking of
    1.12 -source positions.  INCOMPATIBILITY, need to wrap old bstring values
    1.13 -into Binding.name, or better pass through abstract bindings
    1.14 -everywhere.  See further src/Pure/General/long_name.ML,
    1.15 +qualification (by packages and local theory targets), as well as
    1.16 +proper tracking of source positions.  INCOMPATIBILITY, need to wrap
    1.17 +old bstring values into Binding.name, or better pass through abstract
    1.18 +bindings everywhere.  See further src/Pure/General/long_name.ML,
    1.19  src/Pure/General/binding.ML and src/Pure/General/name_space.ML
    1.20  
    1.21  * Simplified interface for defining document antiquotations via