[isabelle-dev] [isabelle] General code_abort'd constant
andreas.lochbihler at inf.ethz.ch
Fri Sep 20 10:47:16 CEST 2013
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.
More information about the isabelle-dev