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