diff -r b13da5649bf9 -r 2cb6ff394bfb NEWS
--- a/NEWS	Tue Apr 13 07:48:32 2004 +0200
+++ b/NEWS	Tue Apr 13 09:42:40 2004 +0200
@@ -85,13 +85,17 @@
   - Rule sets <locale>.intro and <locale>.axioms no longer declared as
     [intro?] and [elim?] (respectively) by default.
   - Experimental command for instantiation of locales in proof contexts:
-        instantiate <label>: <loc>
+        instantiate <label>[<attrs>]: <loc>
     Instantiates locale <loc> and adds all its theorems to the current context
-    taking into account their attributes, and qualifying their names with
-    <label>.  If the locale has assumptions, a chained fact of the form
+    taking into account their attributes.  Label and attrs are optional
+    modifiers, like in theorem declarations.  If present, names of
+    instantiated theorems are qualified with <label>, and the attributes
+    <attrs> are applied after any attributes these theorems might have already.
+      If the locale has assumptions, a chained fact of the form
     "<loc> t1 ... tn" is expected from which instantiations of the parameters
-    are derived.
-    A few (very simple) examples can be found in FOL/ex/LocaleInst.thy.
+    are derived.  The command does not support old-style locales declared
+    with "locale (open)".
+      A few (very simple) examples can be found in FOL/ex/LocaleInst.thy.
 
 * HOL: Tactic emulation methods induct_tac and case_tac understand static
   (Isar) contexts.