NEWS
changeset 66310 e8d2862ec203
parent 66298 5ff9fe3fee66
child 66345 882abe912da9
     1.1 --- a/NEWS	Thu Aug 03 07:31:25 2017 +0200
     1.2 +++ b/NEWS	Wed Aug 02 20:33:39 2017 +0200
     1.3 @@ -99,9 +99,20 @@
     1.4  
     1.5  * Deleting the last code equations for a particular function using
     1.6  [code del] results in function with no equations (runtime abort) rather
     1.7 -than an unimplemented function (generate time abort).  Use explicit
     1.8 +than an unimplemented function (generation time abort).  Use explicit
     1.9  [[code drop:]] to enforce the latter.  Minor INCOMPATIBILTIY.
    1.10  
    1.11 +* Proper concept of code declarations in code.ML:
    1.12 +  - Regular code declarations act only on the global theory level,
    1.13 +    being ignored with warnings if syntactically malformed.
    1.14 +  - Explicitly global code declarations yield errors if syntactically malformed.
    1.15 +  - Default code declarations are silently ignored if syntactically malformed.
    1.16 +Minor INCOMPATIBILITY.
    1.17 +
    1.18 +* Clarified and standardized internal data bookkeeping of code declarations:
    1.19 +history of serials allows to track potentially non-monotonous declarations
    1.20 +appropriately.  Minor INCOMPATIBILITY.
    1.21 +
    1.22  
    1.23  *** HOL ***
    1.24