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

Christian Sternagel c-sterna at jaist.ac.jp
Wed Apr 18 03:53:17 CEST 2012


Just for the record: I exclusively use jEdit for several weeks now and 
did quite a lot of actual proofs. My personal opinion: the user 
experience is much nicer than with emacs

* I did not have any complete hangs yet (as with emacs)
* the whole appearance is much nicer (remember, this is my personal
opinion): font, highlighting, ...
* not to forget the browsability (from constants to their
definitions; from ML functions to their modules)
* checking a single theory (in non-batch mode) is MUCH faster than
with emacs

I would not for the world go back to emacs. (Maybe I should mention that 
before Isabelle I did not use emacs at all, so it was quite annoying to 
have to learn an "operating system" when I just needed an editor ;)).

cheers

chris

On 04/18/2012 01:08 AM, Lawrence Paulson wrote:
> I certainly care about it. Jedit is great for browsing existing theory developments, but there is no support for actually doing proofs.
> Larry
>
> On 17 Apr 2012, at 16:56, Makarius wrote:
>
>>
>> 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.
>>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev




More information about the isabelle-dev mailing list