NEWS
changeset 61681 ca53150406c9
parent 61660 78b371644654
child 61682 f2c69a221055
     1.1 --- a/NEWS	Sat Nov 14 18:37:49 2015 +0100
     1.2 +++ b/NEWS	Sun Nov 15 12:39:51 2015 +0100
     1.3 @@ -529,10 +529,14 @@
     1.4  * Theory Library/Old_Recdef: discontinued obsolete 'defer_recdef'
     1.5  command. Minor INCOMPATIBILITY, use 'function' instead.
     1.6  
     1.7 +* Inductive definitions ('inductive', 'coinductive', etc.) expose
     1.8 +low-level facts of the internal construction only if the option
     1.9 +"inductive_defs" is enabled. This refers to the internal predicate
    1.10 +definition and its monotonicity result. Rare INCOMPATIBILITY.
    1.11 +
    1.12  * Recursive function definitions ('fun', 'function', 'partial_function')
    1.13 -no longer expose the low-level "_def" facts of the internal
    1.14 -construction. INCOMPATIBILITY, enable option "function_defs" in the
    1.15 -context for rare situations where these facts are really needed.
    1.16 +expose low-level facts of the internal construction only if the option
    1.17 +"function_defs" is enabled. Rare INCOMPATIBILITY.
    1.18  
    1.19  * Imperative_HOL: obsolete theory Legacy_Mrec has been removed.
    1.20