NEWS
changeset 62107 f74a33b14200
parent 62098 b1b2834bb493
child 62108 0046bacc5f5b
     1.1 --- a/NEWS	Fri Jan 08 20:06:48 2016 +0100
     1.2 +++ b/NEWS	Sat Jan 09 12:35:07 2016 +0100
     1.3 @@ -342,6 +342,10 @@
     1.4  * Keyword 'rewrites' identifies rewrite morphisms in interpretation
     1.5  commands. Previously, the keyword was 'where'. INCOMPATIBILITY.
     1.6  
     1.7 +* Special notation \<struct> for the first implicit 'structure' in the context
     1.8 +has been discontinued. Rare INCOMPATIBILITY, use explicit structure name
     1.9 +instead, notably in indexed notation with block-subscript (e.g. \<odot>\<^bsub>A\<^esub>).
    1.10 +
    1.11  * More gentle suppression of syntax along locale morphisms while
    1.12  printing terms. Previously 'abbreviation' and 'notation' declarations
    1.13  would be suppressed for morphisms except term identity. Now