# HG changeset patch
# User kleing
# Date 1117441395 -7200
# Node ID d06dc797573120f18fb1cd26fb1bf752c4791aea
# Parent  c423bb89186def1ef06dfab6002ab058345d50a7
updated para on searching

diff -r c423bb89186d -r d06dc7975731 NEWS
--- a/NEWS	Mon May 30 08:21:58 2005 +0200
+++ b/NEWS	Mon May 30 10:23:15 2005 +0200
@@ -91,12 +91,14 @@
 
 * 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.
+  elim, dest, name:string, simp:term, 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, and simp:term selects
+  all simplification rules whose lhs match term.  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."