NEWS
changeset 50878 2840522a936d
parent 50836 c95af99e003b
child 50991 b3c6c9ef11b8
--- 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 ***