diff -r 7e5b9bbc54d8 -r 79cc595655c0 NEWS
--- a/NEWS	Wed Mar 18 22:41:15 2009 +0100
+++ b/NEWS	Thu Mar 19 11:20:22 2009 +0100
@@ -176,30 +176,28 @@
 * 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".
-
-* 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.
-
-* New command 'find_consts' searches for constants based on type and
-name patterns, e.g.
+* New 'find_theorems' criterion "solves" matching theorems that
+directly solve the current goal.
+
+* Auto solve feature for main theorem statements (cf. option in Proof
+General Isabelle settings menu, enabled by default).  Whenever a new
+goal is stated, "find_theorems solves" is called; any theorems that
+could solve the lemma directly are listed underneath the goal.
+
+* 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
+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"
 
-* New command 'local_setup' is similar to 'setup', but operates on a
-local theory context.
+* Command 'local_setup' is similar to 'setup', but operates on a local
+theory context.
 
 
 *** Document preparation ***