# HG changeset patch
# User nipkow
# Date 1141808791 -3600
# Node ID 307dfa3f9e6668efb880a5cad7c3d32a683dcb3f
# Parent  00b01d4445f76978c3fe00bb239dad9d406a686c
*** empty log message ***

diff -r 00b01d4445f7 -r 307dfa3f9e66 NEWS
--- 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>"