diff -r f735e4027656 -r 3c348f5873f3 NEWS
--- 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 ***