Email Gateway (Aug 18 2022 at 14:19): Email Gateway (Aug 18 2022 at 14:19):From: miramirkhani@ce.sharif.edu
Hello all,
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?
Any help would be great.
Thanks
Email Gateway (Aug 18 2022 at 14:20):From: Makarius <makarius@sketis.net>
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
Last updated: Apr 25 2024 at 16:19 UTC