7 See the NEWS file in the distribution for details on user-relevant |
7 See the NEWS file in the distribution for details on user-relevant |
8 changes. |
8 changes. |
9 |
9 |
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-style platform (e.g. Linux, |
13 following additional software: |
13 Windows with Cygwin, Mac OS) and depends on the following main |
|
14 add-on tools: |
14 |
15 |
15 * The Poly/ML compiler and runtime system (version 5.x). |
16 * The Poly/ML compiler and runtime system (version 5.x). |
16 * The GNU bash shell (version 3.x or 2.x). |
17 * The GNU bash shell (version 3.x or 2.x). |
17 * Perl (version 5.x). |
18 * Perl (version 5.x). |
18 * GNU Emacs (version 22) -- for the Proof General interface. |
19 * GNU Emacs (version 22) -- for the Proof General interface. |
19 * A complete LaTeX installation -- for document preparation. |
20 * A complete LaTeX installation -- for document preparation. |
20 |
21 |
21 Installation |
22 Installation |
22 |
23 |
23 Binary packages are available for Isabelle/HOL and ZF for several |
24 Binary packages are available for Isabelle/HOL etc. for several |
24 platforms from the Isabelle web page. The system may be also built |
25 platforms from the Isabelle web page. The system may be also built |
25 from scratch, using the tar.gz source distribution. See file |
26 from scratch, using the tar.gz source distribution. See file |
26 INSTALL as distributed with Isabelle for more information. |
27 INSTALL as distributed with Isabelle for more information. |
27 |
28 |
28 Further background information may be found in the Isabelle System |
29 Further background information may be found in the Isabelle System |
30 |
31 |
31 User interface |
32 User interface |
32 |
33 |
33 The classic Isabelle user interface is Proof General by David |
34 The classic Isabelle user interface is Proof General by David |
34 Aspinall and others. It is a generic Emacs interface for proof |
35 Aspinall and others. It is a generic Emacs interface for proof |
35 assistants, including Isabelle. Proof General is suitable for use |
36 assistants, including Isabelle. Its most prominent feature is |
36 by pacifists and Emacs militants alike. Its most prominent feature |
37 script management, providing a metaphor of stepwise proof script |
37 is script management, providing a metaphor of live proof script |
|
38 editing. Proof General also provides some support for mathematical |
38 editing. Proof General also provides some support for mathematical |
39 symbols displayed on screen. |
39 symbols displayed on screen. |
40 |
40 |
41 Other sources of information |
41 Other sources of information |
42 |
42 |