NEWS
changeset 62109 d65f80949ff1
parent 62108 0046bacc5f5b
child 62111 e2b768b0035d
     1.1 --- a/NEWS	Sat Jan 09 12:58:57 2016 +0100
     1.2 +++ b/NEWS	Sat Jan 09 13:00:04 2016 +0100
     1.3 @@ -14,8 +14,8 @@
     1.4  remains available under print mode "ASCII", but less important syntax
     1.5  has been removed (see below).
     1.6  
     1.7 -* Support for more arrow symbols, with rendering in LaTeX and
     1.8 -Isabelle fonts: \<Lleftarrow> \<Rrightarrow> \<longlongleftarrow> \<longlongrightarrow> \<longlonglongleftarrow> \<longlonglongrightarrow>
     1.9 +* Support for more arrow symbols, with rendering in LaTeX and Isabelle
    1.10 +fonts: \<Lleftarrow> \<Rrightarrow> \<longlongleftarrow> \<longlongrightarrow> \<longlonglongleftarrow> \<longlonglongrightarrow>.
    1.11  
    1.12  * Special notation \<struct> for the first implicit 'structure' in the
    1.13  context has been discontinued. Rare INCOMPATIBILITY, use explicit