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

Andreas Lochbihler andreas.lochbihler at inf.ethz.ch
Thu Jul 18 15:53:29 CEST 2013

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]]


   code_abort error_case_for_f

feels more natural than

   declare some_thm_with_error_case_for_f_as_head_symbol [code_abort]


More information about the isabelle-dev mailing list