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

Johannes Hölzl hoelzl at in.tum.de
Tue Jul 9 15:28:25 CEST 2013

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 remove the code equation for test? Otherwise the
resulting program might be non-terminating.

 - Johannes

More information about the isabelle-dev mailing list