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,