[isabelle-dev] Supported Poly/ML versions

[Clemens Ballarin]

On 13 February, 2016 16:22 CET, Makarius <makarius at sketis.net> wrote: 
 
> > IMHO this sounds too obscure to be useful. How many users are actually 
> > aware of that possibility?
> 
> Maybe 2-3 people on this mailing list, but this is only a guess. So lets 
> make a constructive proof and count the people who show up here to say 
> that they knew that already.

I used this a while ago, with the help of Makarius, to debug a looping sublocale invocation.

> It is indeed all very obscure.  Time is better invested in making the 
> Poly/ML 5.6 debugger work for the Pure bootstrap as well, and add some 
> explicit support for exceptions to it.

I agree.

Clemens