Re: [isabelle] Isabella proof general

X-symbols has been dropped from proof-general in emacs 23, in favor of
Unicode tokens. I use emacs 23.1, proof-general 4 beta cvs checkouts,
and development snapshots of Isabelle. But getting a working collection
of tools is pretty tricky. :(

For Isabelle 2009, I think the best combination is x-symbols and emacs
22. If you have afs filesystem access, you can see my setup of this at:


See the file "", which sets up paths etc.
If you have a similar unix machine, you might even be able to run it
directly from there (probably slowly!).

But you can use that as a template for making your own local installation.


Tim McKenzie wrote:
> On Tue, 27 Oct 2009 09:03:23 Makarius wrote:
>> GNU Emacs 22 or 23 usually works best with Proof General, which
>>  is the default Isabelle user interface that you are faced
>>  with.
> I couldn't get X-Symbol to work in GNU Emacs 23, so I went back to 
> GNU Emacs 22.  Have other people got it working in Emacs 23, or is 
> X-Symbol no longer preferred?
> Tim
> <><

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

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