--- 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.