diff -r ecf1d5d87e5e -r cf6a78acf445 NEWS
--- a/NEWS	Tue Oct 09 17:33:46 2012 +0200
+++ b/NEWS	Wed Oct 10 13:03:50 2012 +0200
@@ -134,6 +134,10 @@
 appear in a constant's type. This alternative to adding TYPE('a) as
 another parameter avoids unnecessary closures in generated code.
 
+* Library/RBT_Impl.thy: efficient construction of red-black trees 
+from sorted associative lists. Merging two trees with rbt_union may
+return a structurally different tree than before. MINOR INCOMPATIBILITY.
+
 * Simproc "finite_Collect" rewrites set comprehensions into pointfree
 expressions.