# HG changeset patch
# User wenzelm
# Date 1190838464 -7200
# Node ID 92767beff42df1bb3534a8cec9c617eaae8348af
# Parent  3a55ee2cae70444e22c0df642db7fa896b7ad6fb
tuned;

diff -r 3a55ee2cae70 -r 92767beff42d NEWS
--- a/NEWS	Wed Sep 26 22:21:05 2007 +0200
+++ b/NEWS	Wed Sep 26 22:27:44 2007 +0200
@@ -407,8 +407,8 @@
 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
+* Pure/Isar: unified syntax for new-style specification mechanisms (e.g.
+'definition', 'abbreviation', or 'inductive' in HOL) admits type
 inference and dummy patterns ("_"). For example:
 
   definition "K x _ = x"