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

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/
(found at the bottom of
http://isabelle.in.tum.de/index.html)

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 <http://isabelle.in.tum.de/dist/Isabelle2013/doc/tutorial.pdf>: http://isabelle.in.tum.de/dist/Isabelle2013/doc/tutorial.pdf
and
The Isabelle/Isar Reference Manual <http://isabelle.in.tum.de/dist/Isabelle2013/doc/isar-ref.pdf>:
http://isabelle.in.tum.de/dist/Isabelle2013/doc/isar-ref.pdf

(both found at http://isabelle.in.tum.de/documentation.html)

Hope that helps,
Walther

PS: Before copying from PDF to Isabelle/jEdit, you might have a look at
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-March/msg00100.html



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