33 annotated source file is run, typesetting the theory |
33 annotated source file is run, typesetting the theory |
34 in the form of a \LaTeX\ source file. This book is derived almost entirely |
34 in the form of a \LaTeX\ source file. This book is derived almost entirely |
35 from output generated in this way. The final chapter of Part~I explains how |
35 from output generated in this way. The final chapter of Part~I explains how |
36 users may produce their own formal documents in a similar fashion. |
36 users may produce their own formal documents in a similar fashion. |
37 |
37 |
38 Isabelle's \hfootref{http://isabelle.in.tum.de/}{web site} contains links to |
38 Isabelle's \hfootref{http://isabelle.in.tum.de/}{web site} contains |
39 the download area and to documentation and other information. Most Isabelle |
39 links to the download area and to documentation and other information. |
40 sessions are now run from within David Aspinall's\index{Aspinall, David} |
40 The classic Isabelle user interface is Proof~General~/ Emacs by David |
41 wonderful user interface, \hfootref{http://proofgeneral.inf.ed.ac.uk/}{Proof |
41 Aspinall's\index{Aspinall, David}. This book says very little about |
42 General}, even together with the |
42 Proof General, which has its own documentation. |
43 \hfootref{http://x-symbol.sourceforge.net}{X-Symbol} package for XEmacs. This |
|
44 book says very little about Proof General, which has its own documentation. |
|
45 In order to run Isabelle, you will need a Standard ML compiler. We recommend |
|
46 \hfootref{http://www.polyml.org/}{Poly/ML}, which is free and gives the best |
|
47 performance. The other fully supported compiler is |
|
48 \hfootref{http://www.smlnj.org/index.html}{Standard ML of New Jersey}. |
|
49 |
43 |
50 This tutorial owes a lot to the constant discussions with and the valuable |
44 This tutorial owes a lot to the constant discussions with and the valuable |
51 feedback from the Isabelle group at Munich: Stefan Berghofer, Olaf |
45 feedback from the Isabelle group at Munich: Stefan Berghofer, Olaf |
52 M{\"u}ller, Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, |
46 M{\"u}ller, Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, |
53 Cornelia Pusch, Norbert Schirmer and Martin Strecker. Stephan |
47 Cornelia Pusch, Norbert Schirmer and Martin Strecker. Stephan |