NEWS

--- a/NEWS	Sun Apr 17 19:40:43 2005 +0200
+++ b/NEWS	Mon Apr 18 09:25:23 2005 +0200
@@ -163,6 +163,7 @@
   do not occur in proof obligations, neither are instantiated theorems stored
   in duplicate.
   Use print_interps to inspect active interpretations of a particular locale.
+  For details, see the Isar Reference manual.
 
 * Locales: proper static binding of attribute syntax -- i.e. types /
   terms / facts mentioned as arguments are always those of the locale