NEWS
changeset 21256 47195501ecf7
parent 21241 a00a16cbc647
child 21265 b8db43faaf9e
--- a/NEWS	Wed Nov 08 22:24:54 2006 +0100
+++ b/NEWS	Wed Nov 08 23:11:13 2006 +0100
@@ -615,9 +615,9 @@
 * inductive and datatype: provide projections of mutual rules, bundled
 as foo_bar.inducts;
 
-* Library: theory Infinite_Set has been moved to the library.
-
-* Library: theory Accessible_Part has been move to main HOL.
+* Library: moved theories Parity, GCD, Binomial, Infinite_Set to Library.
+
+* Library: moved theory Accessible_Part to main HOL.
 
 * Library: added theory Coinductive_List of potentially infinite lists
 as greatest fixed-point.