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:

/afs/inf.ed.ac.uk/group/dreamers/public/software/Isa2009

See the file "source_me.sh", 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.

best,
lucas

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.