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