NEWS
changeset 55524 f41ef840f09d
parent 55519 8a54bf4a92ca
child 55525 70b7e91fa1f9
     1.1 --- a/NEWS	Sun Feb 16 21:33:28 2014 +0100
     1.2 +++ b/NEWS	Sun Feb 16 21:33:28 2014 +0100
     1.3 @@ -129,14 +129,16 @@
     1.4      and "rec_xxx" (e.g., "prod_case" ~> "case_prod").
     1.5      INCOMPATIBILITY.
     1.6  
     1.7 -* The types "'a list" and "'a option", their set and map functions, and their
     1.8 -  selectors are now produced using the new BNF-based datatype package.
     1.9 +* The types "'a list" and "'a option", their set and map functions, their
    1.10 +  relators, and their selectors are now produced using the new BNF-based datatype
    1.11 +  package.
    1.12    Renamed constants:
    1.13      Option.set ~> set_option
    1.14      Option.map ~> map_option
    1.15    Renamed theorems:
    1.16      map_def ~> map_rec[abs_def]
    1.17      Option.map_def ~> map_option_case[abs_def] (with "case_option" instead of "rec_option")
    1.18 +    list_all2_def ~> list_all2_iff
    1.19      map.simps ~> list.map
    1.20      hd.simps ~> list.sel(1)
    1.21      tl.simps ~> list.sel(2-3)