Hi Jasmin,
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.
Andreas
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
