NEWS
authorkuncar
Mon Jan 14 14:03:24 2013 +0100 (2013-01-14)
changeset 508782840522a936d
parent 50877 a2a1a5907f7b
child 50879 fc394c83e490
NEWS
NEWS
     1.1 --- a/NEWS	Mon Jan 14 13:43:58 2013 +0100
     1.2 +++ b/NEWS	Mon Jan 14 14:03:24 2013 +0100
     1.3 @@ -162,6 +162,14 @@
     1.4  switched on by default, and can be switched off by setting the
     1.5  configuration quickcheck_optimise_equality to false.
     1.6  
     1.7 +* Quotient: only one quotient can be defined by quotient_type
     1.8 +INCOMPATIBILITY.
     1.9 +
    1.10 +* Lifting:
    1.11 +  - generation of an abstraction function equation in lift_definition
    1.12 +  - quot_del attribute
    1.13 +  - renamed no_abs_code -> no_code (INCOMPATIBILITY.)
    1.14 +
    1.15  * Simproc "finite_Collect" rewrites set comprehensions into pointfree
    1.16  expressions.
    1.17  
    1.18 @@ -371,6 +379,19 @@
    1.19  with support for mixed, nested recursion and interesting non-free
    1.20  datatypes.
    1.21  
    1.22 +* HOL/Finite_Set and Relation: added new set and relation operations 
    1.23 +expressed by Finite_Set.fold.
    1.24 +
    1.25 +* New theory HOL/Library/RBT_Set: implementation of sets by red-black
    1.26 +trees for the code generator.
    1.27 +
    1.28 +* HOL/Library/RBT and HOL/Library/Mapping have been converted to
    1.29 +Lifting/Transfer.
    1.30 +possible INCOMPATIBILITY.
    1.31 +
    1.32 +* HOL/Set: renamed Set.project -> Set.filter
    1.33 +INCOMPATIBILITY.
    1.34 +
    1.35  
    1.36  *** Document preparation ***
    1.37