# HG changeset patch
# User blanchet
# Date 1514974001 -3600
# Node ID 641d7da6ff96634b0a59c08604bc1e5f4772d205
# Parent  51a7c90fbf19107f219d602d32e06d015d1b8583
updated NEWS

diff -r 51a7c90fbf19 -r 641d7da6ff96 NEWS
--- a/NEWS	Wed Jan 03 11:06:36 2018 +0100
+++ b/NEWS	Wed Jan 03 11:06:41 2018 +0100
@@ -146,6 +146,10 @@
     presence of higher-order quantifiers. An 'smt_explicit_application'
     option has been added to control this. INCOMPATIBILITY.
 
+* Datatypes:
+  - The legacy command 'old_datatype', provided by
+    '~~/src/HOL/Library/Old_Datatype.thy', has been removed. INCOMPATIBILITY.
+
 * Theory HOL-Computational_Algebra.Polynomial_Factorial does not provide
 instances of rat, real, complex as factorial rings etc. Import
 HOL-Computational_Algebra.Field_as_Ring explicitly in case of need.