NEWS
changeset 55875 6478b12b7297
parent 55867 79b915f26533
child 55889 6bfbec3dff62
     1.1 --- a/NEWS	Mon Mar 03 12:58:17 2014 +0100
     1.2 +++ b/NEWS	Mon Mar 03 14:22:35 2014 +0100
     1.3 @@ -112,8 +112,7 @@
     1.4  
     1.5  * Moved new (co)datatype package and its dependencies from "HOL-BNF" to "HOL".
     1.6    The "bnf", "wrap_free_constructors", "datatype_new", "codatatype",
     1.7 -  "primrec_new", "primcorec", and "primcorecursive" command are now part of
     1.8 -  "Main".
     1.9 +  "primcorec", and "primcorecursive" commands are now part of "Main".
    1.10    Theory renamings:
    1.11      FunDef.thy ~> Fun_Def.thy (and Fun_Def_Base.thy)
    1.12      Library/Wfrec.thy ~> Wfrec.thy
    1.13 @@ -146,18 +145,26 @@
    1.14    Discontinued theories:
    1.15      BNF/BNF.thy
    1.16      BNF/Equiv_Relations_More.thy
    1.17 -  Renamed commands:
    1.18 -    datatype_new_compat ~> datatype_compat
    1.19 -    primrec_new ~> primrec
    1.20 -    wrap_free_constructors ~> free_constructors
    1.21    INCOMPATIBILITY.
    1.22  
    1.23 +* New datatype package:
    1.24 +  * "primcorec" is fully implemented.
    1.25 +  * Renamed commands:
    1.26 +      datatype_new_compat ~> datatype_compat
    1.27 +      primrec_new ~> primrec
    1.28 +      wrap_free_constructors ~> free_constructors
    1.29 +    INCOMPATIBILITY.
    1.30 +  * The generated constants "xxx_case" and "xxx_rec" have been renamed
    1.31 +    "case_xxx" and "rec_xxx" (e.g., "prod_case" ~> "case_prod").
    1.32 +    INCOMPATIBILITY.
    1.33 +  * The constant "xxx_(un)fold" and related theorems are no longer generated.
    1.34 +    Use "xxx_(co)rec" or define "xxx_(un)fold" manually using "prim(co)rec".
    1.35 +    INCOMPATIBILITY.
    1.36 +
    1.37  * Old datatype package:
    1.38    * The generated theorems "xxx.cases" and "xxx.recs" have been renamed
    1.39      "xxx.case" and "xxx.rec" (e.g., "sum.cases" -> "sum.case").
    1.40      INCOMPATIBILITY.
    1.41 -
    1.42 -* Old and new (co)datatype packages:
    1.43    * The generated constants "xxx_case" and "xxx_rec" have been renamed
    1.44      "case_xxx" and "rec_xxx" (e.g., "prod_case" ~> "case_prod").
    1.45      INCOMPATIBILITY.