NEWS
changeset 26013 8764a1f1253b
parent 26006 c973b4981276
child 26041 c2e15e65165f
--- a/NEWS	Tue Jan 29 18:00:12 2008 +0100
+++ b/NEWS	Wed Jan 30 10:57:44 2008 +0100
@@ -35,6 +35,9 @@
 
 *** HOL ***
 
+* Theorem Inductive.lfp_ordinal_induct generalized to complete lattices.  The
+form set-specific version is available as Inductive.lfp_ordinal_induct_set.
+
 * Theorems "power.simps" renamed to "power_int.simps".
 
 * New class semiring_div provides basic abstract properties of semirings