10 Isabelle requires a regular Unix platform (e.g. GNU Linux) with the |
10 Isabelle requires a regular Unix platform (e.g. GNU Linux) with the |
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) -- for the ProofGeneral interface. |
15 * XEmacs (version 21.4.x) or GNU Emacs (version 21, 22) |
|
16 -- for the ProofGeneral interface. |
16 * A complete LaTeX installation -- for document preparation. |
17 * A complete LaTeX installation -- for document preparation. |
17 |
18 |
18 Installation |
19 Installation |
19 |
20 |
20 Binary packages are available for Isabelle/HOL and ZF for several |
21 Binary packages are available for Isabelle/HOL and ZF for several |
26 Further background information may be found in the Isabelle System |
27 Further background information may be found in the Isabelle System |
27 Manual, distributed with the sources (directory doc). |
28 Manual, distributed with the sources (directory doc). |
28 |
29 |
29 User interface |
30 User interface |
30 |
31 |
31 The canonical Isabelle user interface is [1]Proof General by David |
32 The canonical Isabelle user interface is Proof General by David |
32 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 |
33 assistants, including Isabelle (both for the classic and Isar |
34 assistants, including Isabelle (both for the classic and Isar |
34 version). Proof General is suitable for use by pacifists and Emacs |
35 version). Proof General is suitable for use by pacifists and Emacs |
35 militants alike. Its most prominent feature is script management, |
36 militants alike. Its most prominent feature is script management, |
36 providing a metaphor of live proof script editing. Proof General has |
37 providing a metaphor of live proof script editing. Proof General has |
37 recently gained a rather large following of both beginning and expert |
38 recently gained a rather large following of both beginning and expert |
38 users of Isabelle. |
39 users of Isabelle. |
39 |
40 |
40 Proof General is distributed together with the XEmacs [2]X-Symbol |
41 Proof General is distributed together with the XEmacs X-Symbol |
41 package, which provides a nice way to get proper mathematical symbols |
42 package, which provides a nice way to get proper mathematical symbols |
42 displayed on screen. |
43 displayed on screen. |
43 |
44 |
44 Other sources of information |
45 Other sources of information |
45 |
46 |
46 The Isabelle Page |
47 The Isabelle Page |
47 |
48 |
48 The Isabelle home page may be accessed both from Cambridge and Munich: |
49 The Isabelle home page may be accessed both from Cambridge and Munich: |
49 * [3]http://www.cl.cam.ac.uk/Research/HVG/Isabelle/ |
50 * http://www.cl.cam.ac.uk/Research/HVG/Isabelle/ |
50 * [4]http://isabelle.in.tum.de |
51 * http://isabelle.in.tum.de |
51 |
52 |
52 Mailing list |
53 Mailing list |
53 |
54 |
54 The electronic mailing list isabelle-users@cl.cam.ac.uk provides a |
55 The electronic mailing list isabelle-users@cl.cam.ac.uk provides a |
55 forum for Isabelle users to discuss problems and exchange information. |
56 forum for Isabelle users to discuss problems and exchange information. |
56 To join, send a message to [5]isabelle-users-request@cl.cam.ac.uk. |
57 To join, send a message to isabelle-users-request@cl.cam.ac.uk. |
57 |
58 |
58 Personal mail |
59 Personal mail |
59 |
60 |
60 [6]Lawrence C Paulson |
61 Lawrence C Paulson |
61 Computer Laboratory |
62 Computer Laboratory |
62 University of Cambridge |
63 University of Cambridge |
63 JJ Thomson Avenue |
64 JJ Thomson Avenue |
64 Cambridge CB3 0FD |
65 Cambridge CB3 0FD |
65 England |
66 England |
66 E-mail: [7]lcp@cl.cam.ac.uk |
67 E-mail: lcp@cl.cam.ac.uk |
67 Phone: +44-223-763500 |
68 Phone: +44-223-763500 |
68 Fax: +44-223-334748 |
69 Fax: +44-223-334748 |
69 |
70 |
70 or |
71 or |
71 |
72 |
72 [8]Tobias Nipkow |
73 Tobias Nipkow |
73 Institut für Informatik |
74 Institut fuer Informatik |
74 Technische Universität München |
75 Technische Universitaet Muenchen |
75 Boltzmannstr. 3 |
76 Boltzmannstr. 3 |
76 D-85748 Garching |
77 D-85748 Garching |
77 Germany |
78 Germany |
78 E-mail: [9]nipkow@in.tum.de |
79 E-mail: nipkow@in.tum.de |
79 Phone: +49-89-289-17302 |
80 Phone: +49-89-289-17302 |
80 Fax: +49-89-289-17307 |
81 Fax: +49-89-289-17307 |
81 _________________________________________________________________ |
82 _________________________________________________________________ |
82 |
83 |
83 Please report any problems you encounter. While we shall try to be |
84 Please report any problems you encounter. While we shall try to be |