[isabelle-dev] [isabelle] General code_abort'd constant

[Andreas Lochbihler]

Hi Jasmin,

I moved this thread from users to devel, because we are now referring to changesets ;-).

>> I would appreciate if all these code_aborts that you mention were consolidated to use Code.abort.
>
> I second this. Cf. http://goo.gl/4kR3vu :)
See now 788730ab7da4, which replaces all code_abort in HOL/Library with Code.abort.
There are still two code_aborts in HOL (in Predicate and Enum) that Code.abort should 
subsume, but Code.abort can only be defined in String.thy due to the error message 
parameter it takes, and Predicate and Enum do not import String. As I am not familiar with 
the HOL import graph, I don't know whether one could easily change it such that Code.abort 
is available in Predicate and Enum. But even if it is, this is probably not going to 
happen before the release.

Andreas