# HG changeset patch
# User wenzelm
# Date 1452340804 -3600
# Node ID d65f80949ff1ce5ca5830aff96baef4f9c105cff
# Parent  0046bacc5f5b02139b0e2d5feaf372b4ad6aab91
tuned;

diff -r 0046bacc5f5b -r d65f80949ff1 NEWS
--- 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