# HG changeset patch
# User wenzelm
# Date 1140115142 -3600
# Node ID 19620462f4a69ef69efbfbca96cce3b938f34930
# Parent  6618203f803237eff038a67b5d22ec4b95a7d7a2
tuned;

diff -r 6618203f8032 -r 19620462f4a6 NEWS
--- a/NEWS	Thu Feb 16 19:10:47 2006 +0100
+++ b/NEWS	Thu Feb 16 19:39:02 2006 +0100
@@ -145,6 +145,9 @@
 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.
+
 * Provers/induct: improved internal context management to support
 local fixes and defines on-the-fly.  Thus explicit meta-level
 connectives !! and ==> are rarely required anymore in inductive goals