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

[Andreas Lochbihler]

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
>