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.