diff -r d49ffd9f9662 -r e4d8dea6dfc2 NEWS
--- a/NEWS	Wed Feb 19 10:53:27 2003 +0100
+++ b/NEWS	Thu Feb 20 11:09:48 2003 +0100
@@ -401,6 +401,10 @@
 
 * HOL: canonical cases/induct rules for n-tuples (n = 3..7);
 
+* HOL: consolidated and renamed several theories.  In particular:
+	Ord.thy has been absorbed into HOL.thy
+	String.thy has been absorbed into List.thy
+ 
 * HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A"
 (beware of argument permutation!);
 
@@ -409,7 +413,8 @@
 * HOL/List: "nodups" renamed to "distinct";
 
 * HOL: added "The" definite description operator; move Hilbert's "Eps"
-to peripheral theory "Hilbert_Choice";
+to peripheral theory "Hilbert_Choice"; some INCOMPATIBILITIES:
+  - Ex_def has changed, now need to use some_eq_ex
 
 * HOL: made split_all_tac safe; EXISTING PROOFS MAY FAIL OR LOOP, so
 in this (rare) case use: