| changeset 19572 | a4b3176f19dd |
| parent 19508 | d5236f5b0a71 |
| child 19587 | eb063e7932d7 |
--- a/NEWS Fri May 05 19:32:35 2006 +0200 +++ b/NEWS Fri May 05 21:59:39 2006 +0200 @@ -400,6 +400,8 @@ * inductive and datatype: provide projections of mutual rules, bundled as foo_bar.inducts; +* Library: theory Accessible_Part has been move to main HOL. + * Library: added theory Coinductive_List of potentially infinite lists as greatest fixed-point.