--- 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".