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