There are several good reasons for using Emacs when you're proving theorems with Isabelle. For example, you can retain a complete history of your interaction inside an Emacs buffer, which you can browse or search through. You can use the editing and history mechanism to speed up typing commands to Isabelle. You can conveniently cut and paste in the shell buffer, to edit your completed proofs into an ML batch file, or issue commands kept in a file.
These things are possible just by running Isabelle inside an Emacs shell buffer. Isamode is an Emacs Lisp package which builds on this to provide additional Isabelle-specific editing and interaction facilities. It goes a small way to softening the harshness of Isabelle's text-only user interface; the hope is that it will help make the learning curve for new Isabelle users less steep, whilst at the same time speeding up use for experienced Isabelle users.
The proof state, rule tables and listener are called associated buffers, because each is associated with a particular Isabelle interaction buffer. Each of the associated buffers can each appear in a separate Emacs frame on the screen.
This manual assumes a basic understanding of Isabelle; you should at least have read the Introduction to Isabelle manual.
To get the most from Isamode, you should understand a little about how Emacs lisp packages work, in particular, how to set user options. Emacs is self-documenting, so you can begin from C-h and find out everything! Here are some useful commands:
info
describe-mode
describe-bindings
describe-function
describe-variable
Go to the first, previous, next, last section, table of contents.