# HG changeset patch
# User wenzelm
# Date 1140120938 -3600
# Node ID 7870cf61c4b361fa0ba15b98ccfd919a327aed5a
# Parent  8d83af663714ca2b65d0c04827dabb6de9f84a2d
tuned;

diff -r 8d83af663714 -r 7870cf61c4b3 NEWS
--- a/NEWS	Thu Feb 16 21:12:03 2006 +0100
+++ b/NEWS	Thu Feb 16 21:15:38 2006 +0100
@@ -138,7 +138,7 @@
 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
+parameters implicit and using the original short name.  See also
 HOL/ex/Abstract_NAT.thy for an example of deriving polymorphic
 entities from a monomorphic theory.