# HG changeset patch
# User wenzelm
# Date 1146859179 -7200
# Node ID a4b3176f19dd1cda64fd0fe26e3509ca8d511bb4
# Parent  0d673faf560c8ee14f020d012494d7f78e3d2fcf
* Library: theory Accessible_Part has been move to main HOL.

diff -r 0d673faf560c -r a4b3176f19dd NEWS
--- 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.