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