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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
