1.1 --- a/NEWS	Wed Sep 26 22:21:02 2007 +0200
     1.2 +++ b/NEWS	Wed Sep 26 22:21:05 2007 +0200
     1.3 @@ -399,13 +399,20 @@
     1.4  Presently, abbreviations are only available 'in' a target locale, but
     1.5  not inherited by general import expressions.  Also note that
     1.6  'abbreviation' may be used as a type-safe replacement for 'syntax' +
     1.7 -'translations' in common applications.
     1.8 +'translations' in common applications.  The "no_abbrevs" print mode
     1.9 +prevents folding of abbreviations in term output.
    1.10  
    1.11  Concrete syntax is attached to specified constants in internal form,
    1.12  independently of name spaces.  The parse tree representation is
    1.13  slightly different -- use 'notation' instead of raw 'syntax', and
    1.14  'translations' with explicit "CONST" markup to accommodate this.
    1.15  
    1.16 +* Pure/Isar: unified syntax for new-style specification mechanisms
    1.17 +('definition', 'abbreviation', or 'inductive' in HOL) admits type
    1.18 +inference and dummy patterns ("_"). For example:
    1.19 +
    1.20 +  definition "K x _ = x"
    1.21 +
    1.22  * Pure: command 'print_abbrevs' prints all constant abbreviations of
    1.23  the current context.  Print mode "no_abbrevs" prevents inversion of
    1.24  abbreviations on output.