--- 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 ***