Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
NEWS
changeset 58373 4bdd00a76e54
parent 58368 fe083c681ed8
child 58410 6d46ad54a2ab 
--- 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".
isabelle