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

[Florian Haftmann]

Hi Andreas,

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

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,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130926/0934b0b8/attachment.sig>