Configuring your system for Isabelle
Open a shell and type setup isabelle in it. In future sessions, this
command should be invoked automatically. For this purpose, add the following
line to your shell configuration file (called .cshrc if your shell is
the c-shell or tc-shell):
setup isabelle
You will always run Isabelle by starting emacs, and it is important that you
start emacs from the shell (and not using, say, pop-up menus of your window
manager). But before starting emacs, add the following lines to your
.emacs file:
(load-file "/usr/local/ProofGeneral-3.1/generic/proof-site.el")
(custom-set-variables
'(proof-multiple-frames-enable t)
'(proof-electric-terminator-enable t)
'(proof-toolbar-use-button-enablers t)
'(isabelle-prog-name "isabelle FOL")
'(proof-x-symbol-enable t)
'(query-user-mail-address nil)
'(proof-toolbar-enable t))
(custom-set-faces)
For the first week's exercises, create a working directory and include the
files IFOL.thy and FOL.thy. Now type xemacs ex1.ML and write
use_thy "FOL";
in the file ex1.ML. This will invoke Isabelle in such a way that you
are set up for the first week's exercises.
The course is now finished (February 14, 2003). However, small corrections
might still be done.
Comments? Send an email to J.-G. Smaus. |
|