* Library: theory Accessible_Part has been move to main HOL.

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