[isabelle-dev] Isabelle2013-2 release

[Lawrence Paulson]

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.

Larry

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.