tuned;
authorwenzelm
Mon Mar 09 22:43:25 2009 +0100 (2009-03-09)
changeset 30399a4772a650b4e
parent 30398 d7ac4b7aa590
child 30400 a7a30ba65d0a
tuned;
NEWS
     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