NEWS
changeset 28966 71a7f76b522d
parent 28964 f0044cdeb945
parent 28965 1de908189869
child 29118 d41182a8135c
     1.1 --- a/NEWS	Thu Dec 04 14:17:36 2008 +0100
     1.2 +++ b/NEWS	Thu Dec 04 14:44:07 2008 +0100
     1.3 @@ -61,6 +61,18 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 +* Type Binding.T gradually replaces formerly used type bstring for names
     1.8 +to be bound.  Name space interface for declarations has been simplified:
     1.9 +
    1.10 +  NameSpace.declare: NameSpace.naming
    1.11 +    -> Binding.T -> NameSpace.T -> string * NameSpace.T
    1.12 +  NameSpace.bind: NameSpace.naming
    1.13 +    -> Binding.T * 'a -> 'a NameSpace.table -> string * 'a NameSpace.table
    1.14 +         (*exception Symtab.DUP*)
    1.15 +
    1.16 +See further modules src/Pure/General/binding.ML and
    1.17 +src/Pure/General/name_space.ML
    1.18 +
    1.19  * Module moves in repository:
    1.20      src/Pure/Tools/value.ML ~> src/Tools/
    1.21      src/Pure/Tools/quickcheck.ML ~> src/Tools/