NEWS
changeset 62111 e2b768b0035d
parent 62101 26c0a70f78a3
parent 62109 d65f80949ff1
child 62114 a7cf464933f7
     1.1 --- a/NEWS	Fri Jan 08 17:41:04 2016 +0100
     1.2 +++ b/NEWS	Sat Jan 09 13:31:31 2016 +0100
     1.3 @@ -14,8 +14,18 @@
     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
    1.14 +structure name instead, notably in indexed notation with block-subscript
    1.15 +(e.g. \<odot>\<^bsub>A\<^esub>).
    1.16 +
    1.17 +* The glyph for \<diamond> in the IsabelleText font now corresponds better to its
    1.18 +counterpart \<box> as quantifier-like symbol. A small diamond is available as
    1.19 +\<diamondop>; the old symbol \<struct> loses this rendering and any special
    1.20 +meaning.
    1.21  
    1.22  * Syntax for formal comments "-- text" now also supports the symbolic
    1.23  form "\<comment> text". Command-line tool "isabelle update_cartouches -c" helps