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