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