# HG changeset patch
# User blanchet
# Date 1393852955 -3600
# Node ID 6478b12b7297ee118950100211c3160531f25c54
# Parent  7eff011e2b369cf5f40ca639c2c98b8b7b7444d3
updated NEWS

diff -r 7eff011e2b36 -r 6478b12b7297 NEWS
--- a/NEWS	Mon Mar 03 12:58:17 2014 +0100
+++ b/NEWS	Mon Mar 03 14:22:35 2014 +0100
@@ -112,8 +112,7 @@
 
 * Moved new (co)datatype package and its dependencies from "HOL-BNF" to "HOL".
   The "bnf", "wrap_free_constructors", "datatype_new", "codatatype",
-  "primrec_new", "primcorec", and "primcorecursive" command are now part of
-  "Main".
+  "primcorec", and "primcorecursive" commands are now part of "Main".
   Theory renamings:
     FunDef.thy ~> Fun_Def.thy (and Fun_Def_Base.thy)
     Library/Wfrec.thy ~> Wfrec.thy
@@ -146,18 +145,26 @@
   Discontinued theories:
     BNF/BNF.thy
     BNF/Equiv_Relations_More.thy
-  Renamed commands:
-    datatype_new_compat ~> datatype_compat
-    primrec_new ~> primrec
-    wrap_free_constructors ~> free_constructors
   INCOMPATIBILITY.
 
+* New datatype package:
+  * "primcorec" is fully implemented.
+  * Renamed commands:
+      datatype_new_compat ~> datatype_compat
+      primrec_new ~> primrec
+      wrap_free_constructors ~> free_constructors
+    INCOMPATIBILITY.
+  * The generated constants "xxx_case" and "xxx_rec" have been renamed
+    "case_xxx" and "rec_xxx" (e.g., "prod_case" ~> "case_prod").
+    INCOMPATIBILITY.
+  * The constant "xxx_(un)fold" and related theorems are no longer generated.
+    Use "xxx_(co)rec" or define "xxx_(un)fold" manually using "prim(co)rec".
+    INCOMPATIBILITY.
+
 * Old datatype package:
   * The generated theorems "xxx.cases" and "xxx.recs" have been renamed
     "xxx.case" and "xxx.rec" (e.g., "sum.cases" -> "sum.case").
     INCOMPATIBILITY.
-
-* Old and new (co)datatype packages:
   * The generated constants "xxx_case" and "xxx_rec" have been renamed
     "case_xxx" and "rec_xxx" (e.g., "prod_case" ~> "case_prod").
     INCOMPATIBILITY.