updated NEWS etc with "solves" criterion and auto_solves

--- a/CONTRIBUTORS	Wed Feb 11 10:51:31 2009 +0100
+++ b/CONTRIBUTORS	Wed Feb 11 23:05:58 2009 +1100
@@ -7,6 +7,9 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* February 2008: Timothy Bourke, NICTA
+  "solves" criterion for find_theorems and auto_solve option
+
 * December 2008: Clemens Ballarin, TUM
   New locale implementation.
 

--- a/NEWS	Wed Feb 11 10:51:31 2009 +0100
+++ b/NEWS	Wed Feb 11 23:05:58 2009 +1100
@@ -183,6 +183,16 @@
 * 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_theorm solves".
+
+* Added an auto solve option, which can be enabled through the
+  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.
+
 
 *** Document preparation ***