--- a/NEWS Sat Jan 09 12:58:57 2016 +0100
+++ b/NEWS Sat Jan 09 13:00:04 2016 +0100
@@ -14,8 +14,8 @@
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