# HG changeset patch
# User kleing
# Date 1114767629 -7200
# Node ID abff581e1d833e9cfb3d392e55b3ce03be382472
# Parent  a191d2bee3e113bda7a2806fe9258e6fe88b93db
new thms_containing that searches for patterns instead of constants
(by Rafal Kolanski, NICTA)

diff -r a191d2bee3e1 -r abff581e1d83 NEWS
--- 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,