NEWS
changeset 49770 cf6a78acf445
parent 49739 13aa6d8268ec
child 49822 0cfc1651be25
     1.1 --- a/NEWS	Tue Oct 09 17:33:46 2012 +0200
     1.2 +++ b/NEWS	Wed Oct 10 13:03:50 2012 +0200
     1.3 @@ -134,6 +134,10 @@
     1.4  appear in a constant's type. This alternative to adding TYPE('a) as
     1.5  another parameter avoids unnecessary closures in generated code.
     1.6  
     1.7 +* Library/RBT_Impl.thy: efficient construction of red-black trees 
     1.8 +from sorted associative lists. Merging two trees with rbt_union may
     1.9 +return a structurally different tree than before. MINOR INCOMPATIBILITY.
    1.10 +
    1.11  * Simproc "finite_Collect" rewrites set comprehensions into pointfree
    1.12  expressions.
    1.13