# HG changeset patch
# User blanchet
# Date 1411051660 -7200
# Node ID 4bdd00a76e54c4073dbebda78042b042d5357a6d
# Parent  bfd497f2f4c253238d3d59b77f6d05bc5702d1ae
updated NEWS

diff -r bfd497f2f4c2 -r 4bdd00a76e54 NEWS
--- a/NEWS	Thu Sep 18 16:47:40 2014 +0200
+++ b/NEWS	Thu Sep 18 16:47:40 2014 +0200
@@ -33,9 +33,11 @@
 Minor INCOMPATIBILITY.
 
 * New (co)datatype package:
-  - The 'datatype_new' command has been renamed 'datatype'. The old command of
-    that name is now called 'old_datatype'. See 'isabelle doc datatypes' for
-    information on porting.
+  - The 'datatype_new' command has been renamed 'datatype'. The old
+    command of that name is now called 'old_datatype' and is provided
+    by "~~/src/HOL/Library/Old_Datatype.thy". See
+    'isabelle doc datatypes' for information on porting.
+    INCOMPATIBILITY.
   - Renamed theorems:
       disc_corec ~> corec_disc
       disc_corec_iff ~> corec_disc_iff
@@ -67,11 +69,16 @@
 
 * Old datatype package:
   - The old 'datatype' command has been renamed 'old_datatype', and
-    'rep_datatype' has been renamed 'old_rep_datatype'. See
+    'rep_datatype' has been renamed 'old_rep_datatype'. They are
+    provided by "~~/src/HOL/Library/Old_Datatype.thy". See
     'isabelle doc datatypes' for information on porting.
+    INCOMPATIBILITY.
   - Renamed theorems:
       weak_case_cong ~> case_cong_weak
     INCOMPATIBILITY.
+  - Renamed theory:
+      ~~/src/HOL/Datatype.thy ~> ~~/src/HOL/Library/Old_Datatype.thy
+    INCOMPATIBILITY.
 
 * Product over lists via constant "listprod".