[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.


--
  Peter






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