# HG changeset patch
# User wenzelm
# Date 1165761031 -3600
# Node ID 0c65e072f4beb8f6e7cf33e030fc9a0c33c6f7de
# Parent  283461c15fa70fefdfa3a427efa1159a56b960fc
added print_abbrevs;
tuned;

diff -r 283461c15fa7 -r 0c65e072f4be NEWS
--- a/NEWS	Sun Dec 10 13:14:43 2006 +0100
+++ b/NEWS	Sun Dec 10 15:30:31 2006 +0100
@@ -15,8 +15,8 @@
 with Isar theories; migration is usually quite simple with the ML
 function use_legacy_bindings.  INCOMPATIBILITY.
 
-* Theory syntax: some popular names (e.g. "class", "if", "fun") are
-now keywords.  INCOMPATIBILITY, use double quotes.
+* Theory syntax: some popular names (e.g. "class", "fun", "help",
+"if") are now keywords.  INCOMPATIBILITY, use double quotes.
 
 * Legacy goal package: reduced interface to the bare minimum required
 to keep existing proof scripts running.  Most other user-level
@@ -54,7 +54,7 @@
 
 * Added antiquotation @{abbrev "c args"} which prints the abbreviation
 "c args == rhs" given in the current context.  (Any number of
-arguments on the LHS may be given.)
+arguments may be given on the LHS.)
 
 
 
@@ -287,6 +287,10 @@
 slightly different -- use 'notation' instead of raw 'syntax', and
 'translations' with explicit "CONST" markup to accommodate this.
 
+* Pure: command 'print_abbrevs' prints all constant abbreviations of
+the current context.  Print mode "no_abbrevs" prevents inversion of
+abbreviations on output.
+
 * Isar/locales: improved parameter handling:
 - use of locales "var" and "struct" no longer necessary;
 - parameter renamings are no longer required to be injective.