10 System requirements |
10 System requirements |
11 |
11 |
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 |
14 |
15 * A full Standard ML Compiler (works best with Poly/ML 5.3.0). |
15 * The Poly/ML compiler and runtime system (version 5.x). |
16 * The GNU bash shell (version 3.x or 2.x). |
16 * The GNU bash shell (version 3.x or 2.x). |
17 * Perl (version 5.x). |
17 * Perl (version 5.x). |
18 * GNU Emacs (version 22 or 23) -- for the Proof General interface. |
18 * GNU Emacs (version 22) -- 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 also built |
25 built from scratch, using the tar.gz source distribution. See file |
25 from scratch, using the tar.gz source distribution. See file |
26 INSTALL as distributed with Isabelle for more information. |
26 INSTALL as distributed with Isabelle for more information. |
27 |
27 |
28 Further background information may be found in the Isabelle System |
28 Further background information may be found in the Isabelle System |
29 Manual, distributed with the sources (directory doc). |
29 Manual, distributed with the sources (directory doc). |
30 |
30 |
31 User interface |
31 User interface |
32 |
32 |
33 The main Isabelle user interface is Proof General by David Aspinall |
33 The classic Isabelle user interface is Proof General by David |
34 and others. It is a generic Emacs interface for proof assistants, |
34 Aspinall and others. It is a generic Emacs interface for proof |
35 including Isabelle. Proof General is suitable for use by pacifists |
35 assistants, including Isabelle. Proof General is suitable for use |
36 and Emacs militants alike. Its most prominent feature is script |
36 by pacifists and Emacs militants alike. Its most prominent feature |
37 management, providing a metaphor of live proof script editing. |
37 is script management, providing a metaphor of live proof script |
38 Proof General also provides some support for mathematical symbols |
38 editing. Proof General also provides some support for mathematical |
39 displayed on screen. |
39 symbols displayed on screen. |
40 |
40 |
41 Other sources of information |
41 Other sources of information |
42 |
42 |
43 The Isabelle Page |
43 The Isabelle Page |
44 |
44 |