diff -r d06fc840a34c -r 786c5f838b0c NEWS
--- a/NEWS	Wed May 18 10:47:25 2005 +0200
+++ b/NEWS	Wed May 18 10:51:15 2005 +0200
@@ -89,10 +89,20 @@
 * Pure: new flag show_question_marks controls printing of leading
   question marks in schematic variable names.
 
-* Pure: new version of thms_containing that searches for a list 
-  of patterns instead of a list of constants. Available in 
-  ProofGeneral under ProofGeneral -> Find Theorems or C-c C-f. 
-  Example search: "(_::nat) + _ + _"   "_ ==> _"
+* Pure: new version of thms_containing that searches for a list of
+  criteria instead of a list of constants. Known criteria are: intro,
+  elim, dest, name:string, and any term. Criteria can be preceded by
+  '-' to select theorems that do not match. Intro, elim, dest select
+  theorems that match the current goal, name:s selects theorems whose
+  fully qualified name contain s.  Any other term is interpreted as
+  pattern and selects all theorem matching the pattern. Available in
+  ProofGeneral under ProofGeneral -> Find Theorems or C-c C-f.
+
+  Example: C-c C-f (100) "(_::nat) + _ + _" intro -name:"HOL."
+
+  prints the last 100 theorems matching the pattern "(_::nat) + _ + _",
+  matching the current goal as introduction rule and not having "HOL." 
+  in their name (i.e. not being defined in theory HOL).
 
 * Pure/Syntax: inner syntax includes (*(*nested*) comments*).