--- a/NEWS Tue Mar 07 18:02:11 2006 +0100
+++ b/NEWS Wed Mar 08 10:06:31 2006 +0100
@@ -328,9 +328,6 @@
*** HOL ***
-* Prefer ex1I over ex_ex1I in single-step reasoning, e.g. by the
-'rule' method.
-
* Alternative iff syntax "A <-> B" for equality on bool (with priority
25 like -->); output depends on the "iff" print_mode, the default is
"A = B" (with priority 50).
@@ -343,6 +340,11 @@
* "m dvd n" where m and n are numbers is evaluated to True/False by simp.
+* Theorem Cons_eq_map_conv no longer has attribute `simp'.
+
+* Prefer ex1I over ex_ex1I in single-step reasoning, e.g. by the
+'rule' method.
+
* Tactics 'sat' and 'satx' reimplemented, several improvements: goals
no longer need to be stated as "<prems> ==> False", equivalences (i.e.
"=" on type bool) are handled, variable names of the form "lit_<n>"