tuned for release;
authorwenzelm
Fri Apr 17 14:57:25 2015 +0200 (2015-04-17)
changeset 60114caf2637a28a9
parent 60113 63194f9141b9
child 60115 9a1c6587e6c1
tuned for release;
NEWS
     1.1 --- a/NEWS	Fri Apr 17 14:30:02 2015 +0200
     1.2 +++ b/NEWS	Fri Apr 17 14:57:25 2015 +0200
     1.3 @@ -198,15 +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 +  - Lifting and Transfer setup for basic HOL types sum and prod (also
    1.13 +    option) is now performed by the BNF package. Theories Lifting_Sum,
    1.14 +    Lifting_Product and Lifting_Option from Main became obsolete and
    1.15 +    were removed. Changed definitions of the relators rel_prod and
    1.16 +    rel_sum (using inductive).
    1.17      INCOMPATIBILITY: use rel_prod.simps and rel_sum.simps instead
    1.18 -      of rel_prod_def and rel_sum_def.
    1.19 -    Minor INCOMPATIBILITY: (rarely used by name) transfer theorem
    1.20 -      names changed (e.g. map_prod_transfer ~> prod.map_transfer).
    1.21 +    of rel_prod_def and rel_sum_def.
    1.22 +    Minor INCOMPATIBILITY: (rarely used by name) transfer theorem names
    1.23 +    changed (e.g. map_prod_transfer ~> prod.map_transfer).
    1.24  
    1.25  * Old datatype package:
    1.26    - The old 'datatype' command has been renamed 'old_datatype', and