NEWS
changeset 19032 d25dfb797612
parent 19006 2427684c201c
child 19034 db16746a5604
equal deleted inserted replaced
19031:0059b5b195a2 19032:d25dfb797612
   355   val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
   355   val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
   356 
   356 
   357 Note that fold_index starts counting at index 0, not 1 like foldln
   357 Note that fold_index starts counting at index 0, not 1 like foldln
   358 used to.
   358 used to.
   359 
   359 
   360 * Pure/General: name_mangler.ML provides a functor for generic name
   360 * Pure/General/name_mangler.ML provides a functor for generic name
   361 mangling (bijective mapping from any expression values to strings).
   361 mangling (bijective mapping from any expression values to strings).
   362 
   362 
   363 * Pure/General: rat.ML implements rational numbers.
   363 * Pure/General/rat.ML implements rational numbers.
       
   364 
       
   365 * Pure/General/table.ML: the join operations now works via exceptions
       
   366 DUP/SAME instead of type option.  This is simpler in simple cases, and
       
   367 admits slightly more efficient complex applications.
   364 
   368 
   365 * Pure: datatype Context.generic joins theory/Proof.context and
   369 * Pure: datatype Context.generic joins theory/Proof.context and
   366 provides some facilities for code that works in either kind of
   370 provides some facilities for code that works in either kind of
   367 context, notably GenericDataFun for uniform theory and proof data.
   371 context, notably GenericDataFun for uniform theory and proof data.
   368 
   372