Re: [isabelle] Two problems about emacs and jedit

On 04/12/2013 09:50 AM, jiangdc wrote:
Hello everyone,
I installed Isabelle2013 with emacs23 on Ubuntu 12.04. When I type => or \<Rightarrow>, it converts to a symbol, which looks like a very tiny "=", but not looks like a normal rightarrow. It works, but just does not look so good.

A quick search with "emacs xsymbol" at
(found at the bottom of

shows that there have been lots of problems with mathematical symbols and emacs since ever.
So most of us are happy to have jEdit now.
And when I use jedit, if I typed a key word incorrectly, e.g. typing "shwo" instead of "show", sometimes I can not edit the file any more. I can save the file by mous, but I have to re-open jedit for further editing. This problem also happens several times when I type "with" and "thus" incorrectly several times.

Good practice with Isabelle/jEdit is, to develop the proof document in a way which avoids errors from the very beginning. Isabelle/Isar provides "oops" and "sorry" for that purpose, see for instance

Tutorial on Isabelle/HOL <>:
The Isabelle/Isar Reference Manual <>:

(both found at

Hope that helps,

PS: Before copying from PDF to Isabelle/jEdit, you might have a look at

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