[isabelle] code del and code drop

>From the NEWS file for 2017:

* 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 (generation time abort). Use explicit
[[code drop:]] to enforce the latter. Minor INCOMPATIBILITY.

Can please someone update the code generator tutorial Sec 2.5 (pg 12).
I spent almost half an hour being puzzled why 
  definition [code del]: "foo == ..."
still admitted code generation for foo.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.