12 Isabelle requires a regular Unix platform (e.g. GNU Linux) with the |
12 Isabelle requires a regular Unix platform (e.g. GNU Linux) with the |
13 following additional software: |
13 following additional software: |
14 * A full Standard ML Compiler (works best with Poly/ML 5.2.1). |
14 * A full Standard ML Compiler (works best with Poly/ML 5.2.1). |
15 * The GNU bash shell (version 3.x or 2.x). |
15 * The GNU bash shell (version 3.x or 2.x). |
16 * Perl (version 5.x). |
16 * Perl (version 5.x). |
17 * GNU Emacs (version 21, 22) or XEmacs (version 21.4.x) |
17 * GNU Emacs (version 21, 22, 23) or XEmacs (version 21.4.x) |
18 -- for the Proof General interface. |
18 -- for the Proof General interface. |
19 * A complete LaTeX installation -- for document preparation. |
19 * A complete LaTeX installation -- for document preparation. |
20 |
20 |
21 Installation |
21 Installation |
22 |
22 |
23 Binary packages are available for Isabelle/HOL and ZF for several |
23 Binary packages are available for Isabelle/HOL and ZF for several |
24 platforms from the Isabelle web page. The system may be easily |
24 platforms from the Isabelle web page. The system may be easily |
25 built from scratch as well, taking the traditional tar.gz source |
25 built from scratch, using the tar.gz source distribution. See file |
26 distribution. See file INSTALL as distributed with Isabelle for |
26 INSTALL as distributed with Isabelle for more information. |
27 more information. |
|
28 |
27 |
29 Further background information may be found in the Isabelle System |
28 Further background information may be found in the Isabelle System |
30 Manual, distributed with the sources (directory doc). |
29 Manual, distributed with the sources (directory doc). |
31 |
30 |
32 User interface |
31 User interface |
34 The main Isabelle user interface is Proof General by David Aspinall |
33 The main Isabelle user interface is Proof General by David Aspinall |
35 and others. It is a generic Emacs interface for proof assistants, |
34 and others. It is a generic Emacs interface for proof assistants, |
36 including Isabelle. Proof General is suitable for use by pacifists |
35 including Isabelle. Proof General is suitable for use by pacifists |
37 and Emacs militants alike. Its most prominent feature is script |
36 and Emacs militants alike. Its most prominent feature is script |
38 management, providing a metaphor of live proof script editing. |
37 management, providing a metaphor of live proof script editing. |
39 Proof General also provides some support for proper mathematical |
38 Proof General also provides some support for mathematical symbols |
40 symbols displayed on screen. |
39 displayed on screen. |
41 |
40 |
42 Other sources of information |
41 Other sources of information |
43 |
42 |
44 The Isabelle Page |
43 The Isabelle Page |
45 |
44 |