# HG changeset patch
# User kuncar
# Date 1358168604 -3600
# Node ID 2840522a936dd257dac52213ebef024f6c799b7e
# Parent  a2a1a5907f7ba7988aa99766d956ae4ca41dda70
NEWS

diff -r a2a1a5907f7b -r 2840522a936d NEWS
--- a/NEWS	Mon Jan 14 13:43:58 2013 +0100
+++ b/NEWS	Mon Jan 14 14:03:24 2013 +0100
@@ -162,6 +162,14 @@
 switched on by default, and can be switched off by setting the
 configuration quickcheck_optimise_equality to false.
 
+* Quotient: only one quotient can be defined by quotient_type
+INCOMPATIBILITY.
+
+* Lifting:
+  - generation of an abstraction function equation in lift_definition
+  - quot_del attribute
+  - renamed no_abs_code -> no_code (INCOMPATIBILITY.)
+
 * Simproc "finite_Collect" rewrites set comprehensions into pointfree
 expressions.
 
@@ -371,6 +379,19 @@
 with support for mixed, nested recursion and interesting non-free
 datatypes.
 
+* HOL/Finite_Set and Relation: added new set and relation operations 
+expressed by Finite_Set.fold.
+
+* New theory HOL/Library/RBT_Set: implementation of sets by red-black
+trees for the code generator.
+
+* HOL/Library/RBT and HOL/Library/Mapping have been converted to
+Lifting/Transfer.
+possible INCOMPATIBILITY.
+
+* HOL/Set: renamed Set.project -> Set.filter
+INCOMPATIBILITY.
+
 
 *** Document preparation ***