Re: [isabelle] jEdit apparantly proves False

On Wed, 20 Nov 2013, Manuel Eberl wrote:

* Improved integration of HOL/Falso (see

Personally, I am delighted to see this finally happening, I'd say it's about time. In fact, it may be the one thing that finally gets me to abandon Proof General in favour of jEdit.

Such jokes are funny on 01-Apr, but not for production versions of Isabelle, especially after an unusually long phase of testing release candidates.

As there is a tendency here to blame Isabelle/jEdit versus Isabelle Proof General, I would like to remind that I was responsible for the latter as well.

5 years ago, I started to move away from the TTY model of Proof General, in order to support interactive document processing natively in Isabelle/Scala.

2 years ago, the first stable release of Isabelle/jEdit came out (as part of Isabelle2011-1).

October 2011 also marks the point where I stopped doing any work on Proof General. As I had been the only one to do anything for Proof General over several years, the number has dropped to zero ever since.

People who are still using Proof General should see what they can do themselves to maintain it. I can give some hints how to get involved -- or just look at


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.