--- a/NEWS Wed Mar 11 20:54:03 2009 +0100
+++ b/NEWS Wed Mar 11 23:59:34 2009 +0100
@@ -186,7 +186,7 @@
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
+* New command 'find_consts' searches for constants based on type and
name patterns, e.g.
find_consts "_ => bool"
@@ -198,8 +198,8 @@
find_consts strict: "_ => bool" name: "Int" -"int => int"
-* Linear arithmetic now ignores all inequalities when fast_arith_neq_limit
-is exceeded, instead of giving up entirely.
+* New command 'local_setup' is similar to 'setup', but operates on a
+local theory context.
*** Document preparation ***
@@ -537,6 +537,9 @@
* ATP selection (E/Vampire/Spass) is now via Proof General's settings
menu.
+* Linear arithmetic now ignores all inequalities when
+fast_arith_neq_limit is exceeded, instead of giving up entirely.
+
*** HOL-Algebra ***