NEWS
changeset 62097 634838f919e4
parent 62086 1c0246456ab9
parent 62093 bd73a2279fcd
child 62098 b1b2834bb493
     1.1 --- a/NEWS	Thu Jan 07 17:42:01 2016 +0000
     1.2 +++ b/NEWS	Fri Jan 08 15:49:01 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