# HG changeset patch
# User wenzelm
# Date 1190838065 -7200
# Node ID 3a55ee2cae70444e22c0df642db7fa896b7ad6fb
# Parent  ff617b6711f42d1c8760924663cfe4ba94bfc770
* Pure/Isar: unified specification syntax admits type inference and dummy patterns;
print mode: no_abbrevs;

diff -r ff617b6711f4 -r 3a55ee2cae70 NEWS
--- a/NEWS	Wed Sep 26 22:21:02 2007 +0200
+++ b/NEWS	Wed Sep 26 22:21:05 2007 +0200
@@ -399,13 +399,20 @@
 Presently, abbreviations are only available 'in' a target locale, but
 not inherited by general import expressions.  Also note that
 'abbreviation' may be used as a type-safe replacement for 'syntax' +
-'translations' in common applications.
+'translations' in common applications.  The "no_abbrevs" print mode
+prevents folding of abbreviations in term output.
 
 Concrete syntax is attached to specified constants in internal form,
 independently of name spaces.  The parse tree representation is
 slightly different -- use 'notation' instead of raw 'syntax', and
 'translations' with explicit "CONST" markup to accommodate this.
 
+* Pure/Isar: unified syntax for new-style specification mechanisms
+('definition', 'abbreviation', or 'inductive' in HOL) admits type
+inference and dummy patterns ("_"). For example:
+
+  definition "K x _ = x"
+
 * Pure: command 'print_abbrevs' prints all constant abbreviations of
 the current context.  Print mode "no_abbrevs" prevents inversion of
 abbreviations on output.