NEWS
changeset 21735 0c65e072f4be
parent 21717 410ca6910f6f
child 21791 367477e8458b
     1.1 --- a/NEWS	Sun Dec 10 13:14:43 2006 +0100
     1.2 +++ b/NEWS	Sun Dec 10 15:30:31 2006 +0100
     1.3 @@ -15,8 +15,8 @@
     1.4  with Isar theories; migration is usually quite simple with the ML
     1.5  function use_legacy_bindings.  INCOMPATIBILITY.
     1.6  
     1.7 -* Theory syntax: some popular names (e.g. "class", "if", "fun") are
     1.8 -now keywords.  INCOMPATIBILITY, use double quotes.
     1.9 +* Theory syntax: some popular names (e.g. "class", "fun", "help",
    1.10 +"if") are now keywords.  INCOMPATIBILITY, use double quotes.
    1.11  
    1.12  * Legacy goal package: reduced interface to the bare minimum required
    1.13  to keep existing proof scripts running.  Most other user-level
    1.14 @@ -54,7 +54,7 @@
    1.15  
    1.16  * Added antiquotation @{abbrev "c args"} which prints the abbreviation
    1.17  "c args == rhs" given in the current context.  (Any number of
    1.18 -arguments on the LHS may be given.)
    1.19 +arguments may be given on the LHS.)
    1.20  
    1.21  
    1.22  
    1.23 @@ -287,6 +287,10 @@
    1.24  slightly different -- use 'notation' instead of raw 'syntax', and
    1.25  'translations' with explicit "CONST" markup to accommodate this.
    1.26  
    1.27 +* Pure: command 'print_abbrevs' prints all constant abbreviations of
    1.28 +the current context.  Print mode "no_abbrevs" prevents inversion of
    1.29 +abbreviations on output.
    1.30 +
    1.31  * Isar/locales: improved parameter handling:
    1.32  - use of locales "var" and "struct" no longer necessary;
    1.33  - parameter renamings are no longer required to be injective.