author | huffman |
Tue, 11 May 2010 11:57:14 -0700 | |
changeset 36829 | 909d2680e122 |
parent 36828 | 6a47f043d498 |
child 36830 | 7902dc7ea11d |
--- a/NEWS Tue May 11 11:40:39 2010 -0700 +++ b/NEWS Tue May 11 11:57:14 2010 -0700 @@ -161,6 +161,9 @@ * Theory Library/Coinductive_List has been removed -- superceded by AFP/thys/Coinductive. +* Theory PReal, including the type "preal" and related operations, has +been removed. INCOMPATIBILITY. + * Split off theory Big_Operators containing setsum, setprod, Inf_fin, Sup_fin, Min, Max from theory Finite_Set. INCOMPATIBILITY.