[isabelle-dev] Supported Poly/ML versions

Lawrence Paulson lp15 at cam.ac.uk
Sat Feb 13 15:11:18 CET 2016

A pity that even this one is necessary. Has tracing somehow got worse since then, and can’t that be reversed?

> On 13 Feb 2016, at 13:42, Makarius <makarius at sketis.net> wrote:
>  * Old Poly/ML 5.3.0 is still needed in rare situations to obtain a
>    detailed exception trace. Note that this needs to be done with
>    isabelle_process or isabelle console, since PIDE requires socket I/O
>    and Poly/ML 5.3.0 does not work with that anymore.

More information about the isabelle-dev mailing list