--- 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.