On 13 February, 2016 16:22 CET, Makarius <makar...@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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
