[isabelle-dev] Supported Poly/ML versions

Clemens Ballarin ballarin at in.tum.de
Sun Feb 14 11:14:32 CET 2016

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.


More information about the isabelle-dev mailing list