changeset 35763 | 765f8adf10f9 |
parent 35745 | 1416f568b2b6 |
child 35765 | 09e238561460 |
--- 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.