diff -r 046fe7ddfc4b -r f65a7fa2da6c NEWS
--- a/NEWS	Fri Feb 15 16:09:10 2008 +0100
+++ b/NEWS	Fri Feb 15 16:09:12 2008 +0100
@@ -35,10 +35,15 @@
 
 *** HOL ***
 
+* Theory Nat: definition of <= and < on natural numbers no longer depend
+on well-founded relations.  INCOMPATIBILITY.  Definitions le_def and less_def
+have disappeared.  Consider lemmas not_less [symmetric, where ?'a = nat]
+and less_eq [symmetric] instead.
+
 * Theory Finite_Set: locales ACf, ACIf, ACIfSL and ACIfSLlin (whose purpose 
 mainly if for various fold_set functionals) have been abandoned in favour of
 the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult,
-lower_semilattice (resp. uper_semilattice) and linorder.  INCOMPATIBILITY.
+lower_semilattice (resp. upper_semilattice) and linorder.  INCOMPATIBILITY.
 
 * Theorem Inductive.lfp_ordinal_induct generalized to complete lattices.  The
 form set-specific version is available as Inductive.lfp_ordinal_induct_set.