NEWS
changeset 16868 eaafda56b14c
parent 16860 43abdba4da5c
child 16869 bc98da5727be
equal deleted inserted replaced
16867:cf7d61d56acf 16868:eaafda56b14c
   418     fold f xs1 #> ... #> fold f xsN
   418     fold f xs1 #> ... #> fold f xsN
   419 
   419 
   420 * Pure/term.ML: combinators fold_atyps, fold_aterms, fold_term_types,
   420 * Pure/term.ML: combinators fold_atyps, fold_aterms, fold_term_types,
   421 fold_types traverse types/terms from left to right, observing
   421 fold_types traverse types/terms from left to right, observing
   422 canonical argument order.  Supercedes previous foldl_XXX versions,
   422 canonical argument order.  Supercedes previous foldl_XXX versions,
   423 add_frees, add_vars have been adapted as well: INCOMPATIBILITY.
   423 add_frees, add_vars etc. have been adapted as well: INCOMPATIBILITY.
   424 
   424 
   425 * Pure: output via the Isabelle channels of writeln/warning/error
   425 * Pure: output via the Isabelle channels of writeln/warning/error
   426 etc. is now passed through Output.output, with a hook for arbitrary
   426 etc. is now passed through Output.output, with a hook for arbitrary
   427 transformations depending on the print_mode (cf. Output.add_mode --
   427 transformations depending on the print_mode (cf. Output.add_mode --
   428 the first active mode that provides a output function wins).  Already
   428 the first active mode that provides a output function wins).  Already