Re: [isabelle] Two problems about emacs and jedit
On 04/12/2013 09:50 AM, jiangdc wrote:
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
Tutorial on Isabelle/HOL
The Isabelle/Isar Reference Manual
(both found at http://isabelle.in.tum.de/documentation.html)
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