(low importance) NEWS
authortraytel
Fri Apr 17 13:01:09 2015 +0200 (2015-04-17)
changeset 601113eaa39b3a0b7
parent 60110 82f355352490
child 60113 63194f9141b9
(low importance) NEWS
NEWS
     1.1 --- a/NEWS	Fri Apr 17 12:12:14 2015 +0200
     1.2 +++ b/NEWS	Fri Apr 17 13:01:09 2015 +0200
     1.3 @@ -198,6 +198,15 @@
     1.4        BNF_Constructions_on_Wellorders ~> BNF_Wellorder_Constructions
     1.5        Cardinals/Constructions_on_Wellorders ~> Cardinals/Wellorder_Constructions
     1.6      INCOMPATIBILITY.
     1.7 +  - Lifting and Transfer setup for basic HOL types sum and prod
     1.8 +    (also option) is now performed by the BNF package. Theories
     1.9 +    Lifting_Sum, Lifting_Product and Lifting_Option from Main
    1.10 +    became obsolete and were removed. Changed definitions of
    1.11 +    the relators rel_prod and rel_sum (using inductive).
    1.12 +    INCOMPATIBILITY: use rel_prod.simps and rel_sum.simps instead
    1.13 +      of rel_prod_def and rel_sum_def.
    1.14 +    Minor INCOMPATIBILITY: (rarely used by name) transfer theorem
    1.15 +      names changed (e.g. map_prod_transfer ~> prod.map_transfer).
    1.16  
    1.17  * Old datatype package:
    1.18    - The old 'datatype' command has been renamed 'old_datatype', and