11 following additional software: |
11 following additional software: |
12 * A full Standard ML Compiler (e.g. Poly/ML 5.x, 4.x). |
12 * A full Standard ML Compiler (e.g. Poly/ML 5.x, 4.x). |
13 * The GNU bash shell (version 3.x, 2.x). |
13 * The GNU bash shell (version 3.x, 2.x). |
14 * Perl (version 5.x). |
14 * Perl (version 5.x). |
15 * XEmacs (version 21.4.x) or GNU Emacs (version 21, 22) |
15 * XEmacs (version 21.4.x) or GNU Emacs (version 21, 22) |
16 -- for the ProofGeneral interface. |
16 -- for the Proof General interface. |
17 * A complete LaTeX installation -- for document preparation. |
17 * A complete LaTeX installation -- for document preparation. |
18 |
18 |
19 Installation |
19 Installation |
20 |
20 |
21 Binary packages are available for Isabelle/HOL and ZF for several |
21 Binary packages are available for Isabelle/HOL and ZF for several |
22 platforms from the Isabelle web page. The system may be easily built |
22 platforms from the Isabelle web page. The system may be easily |
23 from scratch as well, taking the traditional tar.gz source |
23 built from scratch as well, taking the traditional tar.gz source |
24 distribution. See file INSTALL as distributed with Isabelle for more |
24 distribution. See file INSTALL as distributed with Isabelle for |
25 information. |
25 more information. |
26 |
26 |
27 Further background information may be found in the Isabelle System |
27 Further background information may be found in the Isabelle System |
28 Manual, distributed with the sources (directory doc). |
28 Manual, distributed with the sources (directory doc). |
29 |
29 |
30 User interface |
30 User interface |
31 |
31 |
32 The canonical Isabelle user interface is Proof General by David |
32 The canonical Isabelle user interface is Proof General by David |
33 Aspinall and others. It is a generic (X)Emacs interface for proof |
33 Aspinall and others. It is a generic (X)Emacs interface for proof |
34 assistants, including Isabelle (both for the classic and Isar |
34 assistants, including Isabelle. Proof General is suitable for use |
35 version). Proof General is suitable for use by pacifists and Emacs |
35 by pacifists and Emacs militants alike. Its most prominent feature |
36 militants alike. Its most prominent feature is script management, |
36 is script management, providing a metaphor of live proof script |
37 providing a metaphor of live proof script editing. Proof General has |
37 editing. |
38 recently gained a rather large following of both beginning and expert |
|
39 users of Isabelle. |
|
40 |
38 |
41 Proof General is distributed together with the XEmacs X-Symbol |
39 Proof General is distributed together with the XEmacs X-Symbol |
42 package, which provides a nice way to get proper mathematical symbols |
40 package, which provides a reasonable way to get proper mathematical |
43 displayed on screen. |
41 symbols displayed on screen. |
44 |
42 |
45 Other sources of information |
43 Other sources of information |
46 |
44 |
47 The Isabelle Page |
45 The Isabelle Page |
48 |
46 |