NEWS
changeset 62108 0046bacc5f5b
parent 62107 f74a33b14200
child 62109 d65f80949ff1
     1.1 --- a/NEWS	Sat Jan 09 12:35:07 2016 +0100
     1.2 +++ b/NEWS	Sat Jan 09 12:58:57 2016 +0100
     1.3 @@ -17,6 +17,16 @@
     1.4  * Support for more arrow symbols, with rendering in LaTeX and
     1.5  Isabelle fonts: \<Lleftarrow> \<Rrightarrow> \<longlongleftarrow> \<longlongrightarrow> \<longlonglongleftarrow> \<longlonglongrightarrow>
     1.6  
     1.7 +* Special notation \<struct> for the first implicit 'structure' in the
     1.8 +context has been discontinued. Rare INCOMPATIBILITY, use explicit
     1.9 +structure name instead, notably in indexed notation with block-subscript
    1.10 +(e.g. \<odot>\<^bsub>A\<^esub>).
    1.11 +
    1.12 +* The glyph for \<diamond> in the IsabelleText font now corresponds better to its
    1.13 +counterpart \<box> as quantifier-like symbol. A small diamond is available as
    1.14 +\<diamondop>; the old symbol \<struct> loses this rendering and any special
    1.15 +meaning.
    1.16 +
    1.17  * Syntax for formal comments "-- text" now also supports the symbolic
    1.18  form "\<comment> text". Command-line tool "isabelle update_cartouches -c" helps
    1.19  to update old sources.
    1.20 @@ -342,10 +352,6 @@
    1.21  * Keyword 'rewrites' identifies rewrite morphisms in interpretation
    1.22  commands. Previously, the keyword was 'where'. INCOMPATIBILITY.
    1.23  
    1.24 -* Special notation \<struct> for the first implicit 'structure' in the context
    1.25 -has been discontinued. Rare INCOMPATIBILITY, use explicit structure name
    1.26 -instead, notably in indexed notation with block-subscript (e.g. \<odot>\<^bsub>A\<^esub>).
    1.27 -
    1.28  * More gentle suppression of syntax along locale morphisms while
    1.29  printing terms. Previously 'abbreviation' and 'notation' declarations
    1.30  would be suppressed for morphisms except term identity. Now