[isabelle-dev] [isabelle] General code_abort'd constant
florian.haftmann at informatik.tu-muenchen.de
Thu Sep 26 17:50:32 CEST 2013
> See now 788730ab7da4, which replaces all code_abort in HOL/Library with
> 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.
Making Predicate.thy dependent on String.thy is no problem. The reason
why Enum.thy is bootstrapped before String.thy is that »enum« allows for
a nice code setup which is also valid in presence of Code_Char.thy.
However you arrange it, there is always one piece of code setup which
cannot be bootstrapped from the beginning.
Hope this helps,
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 263 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev