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

[Andreas Lochbihler]

Hi Florian,

On 18/07/13 15:07, Florian Haftmann wrote:
> The idea is to have an explicit delete declaration, e.g. something like
>
> definition error_case_for_f where [code del]: "error_case_for_f = f"
>
> which will both have the effect of leaving no code equations for
> error_case *and* generate exception code (instead of aborting).
I see, but I recommend that the attribute is not called [code del], but e.g. [code abort].
However, I am not sure whether I like this idea, because an attribute that acts on a 
theorem seems weird, as "generate exception code" is a property of a constant rather than 
a theorem. So I still think that something like

   declare [[code_abort error_case_for_f]]

or

   code_abort error_case_for_f

feels more natural than

   declare some_thm_with_error_case_for_f_as_head_symbol [code_abort]

Best,
Andreas