[isabelle-dev] Supported Poly/ML versions
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.
More information about the isabelle-dev