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