Hi Florian,
in 2b761d9a74f5, I now have replaced Predicate.not_unique with Code.abort. I decided to
leave Enum.the as is, because there is a special translation for the Eval target such that
Enum.the raises Match instead of Fail (although I do not know whether the specific setup
is important).
Andreas
On 26/09/13 17:50, Florian Haftmann wrote:
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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
