# HG changeset patch
# User wenzelm
# Date 1140113447 -3600
# Node ID 6618203f803237eff038a67b5d22ec4b95a7d7a2
# Parent  47532d00e0c8a4cd6f5dd65d7a36e11d0025709d
tuned;

diff -r 47532d00e0c8 -r 6618203f8032 NEWS
--- a/NEWS	Thu Feb 16 18:59:39 2006 +0100
+++ b/NEWS	Thu Feb 16 19:10:47 2006 +0100
@@ -117,8 +117,8 @@
 
 * Isar/locales: new derived specification elements 'definition',
 'abbreviation', 'axiomatization', which support type-inference, admit
-object-level specifications (equality, equivalence), and may used
-within an optional locale context.  For example:
+object-level specifications (equality, equivalence).  See also the
+isar-ref manual.  Examples:
 
   definition
     "f x y = x + y + 1"
@@ -134,14 +134,16 @@
     neq  (infix "=!=" 50)
     "(x =!= y) <-> ~ (x === y)"
 
-Within a locale context, constants being introduced depend on certain
-fixed parameters, and the constant name is qualified by the locale
-base name.  An internal abbreviation takes care for convenient input
-and output, making the parameters implicit and using the original
-short name.  Presently, abbreviations are only available "in" a target
-locale, but not inherited by general import expressions.
-
-See the isar-ref manual for further details.
+These specifications may be also used in a locale context.  Then the
+constants being introduced depend on certain fixed parameters, and the
+constant name is qualified by the locale base name.  An internal
+abbreviation takes care for convenient input and output, making the
+parameters implicit and using the original short name.  See
+HOL/ex/Abstract_NAT.thy for an example of deriving polymorphic
+entities from a monomorphic theory.
+
+Presently, abbreviations are only available 'in' a target locale, but
+not inherited by general import expressions.
 
 * Provers/induct: improved internal context management to support
 local fixes and defines on-the-fly.  Thus explicit meta-level