NEWS
changeset 18642 6954633b6a76
parent 18601 b248754b60bc
child 18644 b59766bc66c9
equal deleted inserted replaced
18641:688056d430b0 18642:6954633b6a76
   294 
   294 
   295 * Pure/General: name_mangler.ML provides a functor for generic name
   295 * Pure/General: name_mangler.ML provides a functor for generic name
   296 mangling (bijective mapping from any expression values to strings).
   296 mangling (bijective mapping from any expression values to strings).
   297 
   297 
   298 * Pure/General: rat.ML implements rational numbers.
   298 * Pure/General: rat.ML implements rational numbers.
       
   299 
       
   300 * Pure: datatype Context.generic joins theory/Proof.context and
       
   301 provides some facilities for generic code that works in either kind of
       
   302 context, notably GenericDataFun for uniform theory and proof data.
       
   303 
       
   304 * Pure: type Context.generic attribute is now the preferred
       
   305 representation for global vs. local attributes while avoiding code
       
   306 duplication; Attrib.theory/context/generic converts between different
       
   307 types of attributes.  Various Pure/HOL/ZF packages work with generic
       
   308 attributes now, INCOMPATIBILITY.
   299 
   309 
   300 * Pure: several functions of signature "... -> theory -> theory * ..."
   310 * Pure: several functions of signature "... -> theory -> theory * ..."
   301 have been reoriented to "... -> theory -> ... * theory" in order to
   311 have been reoriented to "... -> theory -> ... * theory" in order to
   302 allow natural usage in combination with the ||>, ||>>, |-> and
   312 allow natural usage in combination with the ||>, ||>>, |-> and
   303 fold_map combinators.
   313 fold_map combinators.