[isabelle-dev] Isabelle2013-2 release

Lawrence Paulson lp15 at cam.ac.uk
Thu Nov 21 15:19:53 CET 2013

I doubt very much that many people are still using PG.

This wasn’t noticed because there was nothing to notice: the problem is the absence of something, rather than the presence, so it’s subtle and insidious. People may have encountered this problem without realising it.


On 21 Nov 2013, at 11:21, Makarius <makarius at sketis.net> wrote:

> I am a little disturbed that such a serious problem was undetected (or unreported) for such a long time.  It shows that the Isabelle development and release process no longer works reliably -- although I've spent about the same time doing new things in summer versus getting the release ready in autumn.
> Another conclusion is that the majority of serious proof development is still done in Proof General.

More information about the isabelle-dev mailing list