new thms_containing that searches for patterns instead of constants
(by Rafal Kolanski, NICTA)

--- a/NEWS	Fri Apr 29 11:22:41 2005 +0200
+++ b/NEWS	Fri Apr 29 11:40:29 2005 +0200
@@ -124,6 +124,11 @@
 * Pure: new flag show_var_qmarks to control printing of leading
   question marks of 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/Syntax: inner syntax includes (*(*nested*) comments*).
 
 * Pure/Syntax: pretty pinter now supports unbreakable blocks,