added print_abbrevs;
Sun, 10 Dec 2006 15:30:31 +0100
changeset 21735 0c65e072f4be
parent 21734 283461c15fa7
child 21736 ccb2346ee416
added print_abbrevs; tuned;
--- 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.