# HG changeset patch
# User kleing
# Date 1234472370 -39600
# Node ID 14841d4c808e1400f1bc69d43cb916cb4b9dec5e
# Parent  29154e67731d963ede9848a103364b71bfd271ab
added find_consts to NEWS and CONTRIBUTORS

diff -r 29154e67731d -r 14841d4c808e CONTRIBUTORS
--- a/CONTRIBUTORS	Fri Feb 13 07:53:38 2009 +1100
+++ b/CONTRIBUTORS	Fri Feb 13 07:59:30 2009 +1100
@@ -8,6 +8,9 @@
 --------------------------------------
 
 * February 2008: Timothy Bourke, NICTA
+  New find_consts command.
+
+* February 2008: Timothy Bourke, NICTA
   "solves" criterion for find_theorems and auto_solve option
 
 * December 2008: Clemens Ballarin, TUM
diff -r 29154e67731d -r 14841d4c808e NEWS
--- a/NEWS	Fri Feb 13 07:53:38 2009 +1100
+++ b/NEWS	Fri Feb 13 07:59:30 2009 +1100
@@ -183,15 +183,26 @@
 * The 'axiomatization' command now only works within a global theory
 context.  INCOMPATIBILITY.
 
-* New find_theorems criterion "solves" matching theorems that 
-  directly solve the current goal. Try "find_theorems solves".
+* New find_theorems criterion "solves" matching theorems that
+directly solve the current goal. Try "find_theorems solves".
 
 * Added an auto solve option, which can be enabled through the
-  ProofGeneral Isabelle settings menu (disabled by default).
+ProofGeneral Isabelle settings menu (disabled by default).
  
-  When enabled, find_theorems solves is called whenever a new lemma
-  is stated. Any theorems that could solve the lemma directly are
-  listed underneath the goal.
+When enabled, find_theorems solves is called whenever a new lemma is
+stated. Any theorems that could solve the lemma directly are listed
+underneath the goal.
+
+* New command find_consts searches for constants based on type and name 
+patterns, e.g.
+
+    find_consts "_ => bool"
+
+By default, matching is against subtypes, but it may be restricted to the
+whole type. Searching by name is possible. Multiple queries are conjunctive
+and queries may be negated by prefixing them with a hyphen:
+
+    find_consts strict: "_ => bool" name: "Int" -"int => int"
 
 
 *** Document preparation ***