[isabelle-dev] <-> and <-->

[Makarius]

On Tue, 17 Apr 2012, Tobias Nipkow wrote:

> Am 17/04/2012 16:27, schrieb Lawrence Paulson:
>> I think you are right that ASCII syntax is almost completely irrelevant now. Hardly anybody sees it.
>
> It is relevant as an input method, and that is exactly what my 
> suggestion is about. I am not interested in ASCII art but in a smooth 
> input method. When I type, I would prefer to keep on typing.

Why then the proposal to change the prover syntax?

Anyway, who is maintaining Isabelle ProofGeneral now?  The repository 
version does not work with Emacs 23 for several months already.  It seems 
that nobody cares about it anymore.

For the release, I will package up official ProofGeneral-4.1 as last time. 
It is then up to its users to test it and report problems in the usual 
testing stage before the release.


 	Makarius