[isabelle-dev] Should code_abort remove the corresponding code equations?

Hi *, code_abort does not remove the corresponding code equations (in Isabelle 19764bef2730) definition test = True code_abort test value [code] test -- outputs True definition [code del]: test2 = True code_abort test2 value [code] test2 -- raises 'test' exception Should code_abort

Re: [isabelle-dev] Should code_abort remove the corresponding code equations?

Hi Johannes, I have often run into this problem myself, too, especially in case of non-termination. I would find it sensible that code_abort deletes the code equation. Andreas On 09/07/13 15:28, Johannes Hölzl wrote: Hi *, code_abort does not remove the corresponding code equations (in