48 users may produce their own formal documents in a similar fashion. |
48 users may produce their own formal documents in a similar fashion. |
49 |
49 |
50 Isabelle's \hfootref{http://isabelle.in.tum.de/}{web site} contains links to |
50 Isabelle's \hfootref{http://isabelle.in.tum.de/}{web site} contains links to |
51 the download area and to documentation and other information. Most Isabelle |
51 the download area and to documentation and other information. Most Isabelle |
52 sessions are now run from within David Aspinall's\index{Aspinall, David} |
52 sessions are now run from within David Aspinall's\index{Aspinall, David} |
53 wonderful user interface, \hfootref{http://www.proofgeneral.org/}{Proof |
53 wonderful user interface, \hfootref{http://proofgeneral.inf.ed.ac.uk/}{Proof |
54 General}, even together with the |
54 General}, even together with the |
55 \hfootref{http://x-symbol.sourceforge.net}{X-Symbol} package for XEmacs. This |
55 \hfootref{http://x-symbol.sourceforge.net}{X-Symbol} package for XEmacs. This |
56 book says very little about Proof General, which has its own documentation. |
56 book says very little about Proof General, which has its own documentation. |
57 In order to run Isabelle, you will need a Standard ML compiler. We recommend |
57 In order to run Isabelle, you will need a Standard ML compiler. We recommend |
58 \hfootref{http://www.polyml.org/}{Poly/ML}, which is free and gives the best |
58 \hfootref{http://www.polyml.org/}{Poly/ML}, which is free and gives the best |