Re: [isabelle] Inner Lexical Error



On Sun, 8 Nov 2009, miramirkhani at ce.sharif.edu wrote:

I've installed Isabelle on Ubuntu 8.10 and I use isabelle emacs to start
the system. I also turn X-symbol on in Proof General but when I compile
Message.thy(get it from the Isabelle Library 2009 :
http://isabelle.in.tum.de/library/HOL/Auth/NS_Shared.html or other theory
files using math symbols), I get "Inner lexical error" or "Inner Syntax
Error", "Failed to Parse Proposition" at commands which contain \<union>
or existential quantifier(but it can parse \<in> symbol)?!!
What is wrong?

This sounds like one of the usual problems with Emacs + Proof General.

I would say that the GNU Emacs 22 (Gtk) shipped with Ubuntu 8.10 should work together with Proof General 3.7.1 (the one from the Isabelle download site, don't waste time on the prepackaged .deb of Proof General.)

Which versions do you have?


	Makarius






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