--- 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.