--- 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.