updated NEWS
authorblanchet
Wed Apr 23 10:23:27 2014 +0200 (2014-04-23)
changeset 56652b0126a5a256d
parent 56651 fc105315822a
child 56653 c1507d5f4665
updated NEWS
NEWS
     1.1 --- a/NEWS	Wed Apr 23 10:23:27 2014 +0200
     1.2 +++ b/NEWS	Wed Apr 23 10:23:27 2014 +0200
     1.3 @@ -279,6 +279,10 @@
     1.4  
     1.5  * New (co)datatype package:
     1.6    * "primcorec" is fully implemented.
     1.7 +  * "datatype_new" generates size functions ("size_xxx" and "size") as
     1.8 +    required by "fun".
     1.9 +  * BNFs are integrated with the Lifting tool and new-style (co)datatypes
    1.10 +    with Transfer.
    1.11    * Renamed commands:
    1.12        datatype_new_compat ~> datatype_compat
    1.13        primrec_new ~> primrec
    1.14 @@ -306,12 +310,13 @@
    1.15      Option.set ~> set_option
    1.16      Option.map ~> map_option
    1.17      option_rel ~> rel_option
    1.18 -    option_rec ~> case_option
    1.19 +    list_size ~> size_list
    1.20 +    option_size ~> size_option
    1.21    Renamed theorems:
    1.22      set_def ~> set_rec[abs_def]
    1.23      map_def ~> map_rec[abs_def]
    1.24      Option.map_def ~> map_option_case[abs_def] (with "case_option" instead of "rec_option")
    1.25 -    option.recs ~> option.case
    1.26 +    option.recs ~> option.rec
    1.27      list_all2_def ~> list_all2_iff
    1.28      set.simps ~> set_simps (or the slightly different "list.set")
    1.29      map.simps ~> list.map