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. Greetings, - Johannes _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
