NEWS
changeset 67335 641d7da6ff96
parent 67311 3869b2400e22
child 67341 df79ef3b3a41
     1.1 --- a/NEWS	Wed Jan 03 11:06:36 2018 +0100
     1.2 +++ b/NEWS	Wed Jan 03 11:06:41 2018 +0100
     1.3 @@ -146,6 +146,10 @@
     1.4      presence of higher-order quantifiers. An 'smt_explicit_application'
     1.5      option has been added to control this. INCOMPATIBILITY.
     1.6  
     1.7 +* Datatypes:
     1.8 +  - The legacy command 'old_datatype', provided by
     1.9 +    '~~/src/HOL/Library/Old_Datatype.thy', has been removed. INCOMPATIBILITY.
    1.10 +
    1.11  * Theory HOL-Computational_Algebra.Polynomial_Factorial does not provide
    1.12  instances of rat, real, complex as factorial rings etc. Import
    1.13  HOL-Computational_Algebra.Field_as_Ring explicitly in case of need.