--- a/NEWS Fri Jan 08 17:41:04 2016 +0100
+++ b/NEWS Sat Jan 09 13:31:31 2016 +0100
@@ -14,8 +14,18 @@
remains available under print mode "ASCII", but less important syntax
has been removed (see below).
-* Support for more arrow symbols, with rendering in LaTeX and
-Isabelle fonts: \<Lleftarrow> \<Rrightarrow> \<longlongleftarrow> \<longlongrightarrow> \<longlonglongleftarrow> \<longlonglongrightarrow>
+* Support for more arrow symbols, with rendering in LaTeX and Isabelle
+fonts: \<Lleftarrow> \<Rrightarrow> \<longlongleftarrow> \<longlongrightarrow> \<longlonglongleftarrow> \<longlonglongrightarrow>.
+
+* Special notation \<struct> for the first implicit 'structure' in the
+context has been discontinued. Rare INCOMPATIBILITY, use explicit
+structure name instead, notably in indexed notation with block-subscript
+(e.g. \<odot>\<^bsub>A\<^esub>).
+
+* The glyph for \<diamond> in the IsabelleText font now corresponds better to its
+counterpart \<box> as quantifier-like symbol. A small diamond is available as
+\<diamondop>; the old symbol \<struct> loses this rendering and any special
+meaning.
* Syntax for formal comments "-- text" now also supports the symbolic
form "\<comment> text". Command-line tool "isabelle update_cartouches -c" helps