NEWS
changeset 66149 4bf16fb7c14d
parent 66135 1451a32479ba
child 66181 33d7519fc35d
     1.1 --- a/NEWS	Tue Jun 20 13:07:47 2017 +0200
     1.2 +++ b/NEWS	Tue Jun 20 13:07:49 2017 +0200
     1.3 @@ -74,6 +74,14 @@
     1.4  * Update to jedit-5.4.0.
     1.5  
     1.6  
     1.7 +*** Pure ***
     1.8 +
     1.9 +* Deleting the last code equations for a particular function using
    1.10 +[code del] results in function with no equations (runtime abort) rather
    1.11 +than an unimplemented function (generate time abort).  Use explicit
    1.12 +[[code drop:]] to enforce the latter.  Minor INCOMPATIBILTIY.
    1.13 +
    1.14 +
    1.15  *** HOL ***
    1.16  
    1.17  * "sublist" from theory List renamed to "nths" in analogy with "nth".