NEWS

 * Pure: 'print_theory' now suppresses entities with internal name
 (trailing "_") by default; use '!' option for full details.
 
 
 *** HOL ***
+
+* constant "List.op @" now named "List.append".  Use ML antiquotations
+@{const_name List.append} or @{term " ... @ ... "} to circumvent
+possible incompatibilities when working on ML level.
 
 * Constant renames due to introduction of canonical name prefixing for
   class package:
 
     HOL.abs ~> HOL.minus_class.abs