NEWS
changeset 62093 bd73a2279fcd
parent 62084 969119292e25
child 62097 634838f919e4
     1.1 --- a/NEWS	Thu Jan 07 15:50:09 2016 +0100
     1.2 +++ b/NEWS	Thu Jan 07 15:53:39 2016 +0100
     1.3 @@ -443,12 +443,17 @@
     1.4  
     1.5  * Inductive definitions ('inductive', 'coinductive', etc.) expose
     1.6  low-level facts of the internal construction only if the option
     1.7 -"inductive_defs" is enabled. This refers to the internal predicate
     1.8 +"inductive_internals" is enabled. This refers to the internal predicate
     1.9  definition and its monotonicity result. Rare INCOMPATIBILITY.
    1.10  
    1.11  * Recursive function definitions ('fun', 'function', 'partial_function')
    1.12  expose low-level facts of the internal construction only if the option
    1.13 -"function_defs" is enabled. Rare INCOMPATIBILITY.
    1.14 +"function_internals" is enabled. Rare INCOMPATIBILITY.
    1.15 +
    1.16 +* BNF datatypes ('datatype', 'codatatype', etc.) expose low-level facts
    1.17 +of the internal construction only if the option "bnf_internals" is
    1.18 +enabled. This supersedes the former option "bnf_note_all". Rare
    1.19 +INCOMPATIBILITY.
    1.20  
    1.21  * Combinator to represent case distinction on products is named
    1.22  "case_prod", uniformly, discontinuing any input aliasses. Very popular