diff -r af3ff2ba4c54 -r 765f8adf10f9 NEWS
--- a/NEWS	Sat Mar 13 16:44:12 2010 +0100
+++ b/NEWS	Sat Mar 13 17:19:12 2010 +0100
@@ -89,6 +89,9 @@
 contain multiple interpretations of local typedefs (with different
 non-emptiness proofs), even in a global theory context.
 
+* Theory Library/Coinductive_List has been removed -- superceded by
+AFP/thys/Coinductive.
+
 * Split off theory Big_Operators containing setsum, setprod, Inf_fin, Sup_fin,
 Min, Max from theory Finite_Set.  INCOMPATIBILITY.